Automating change of representation for proofs in discrete mathematics

Daniel Raggi; Alan Bundy; Gudmund Grov; Alison Pease

doi:10.1007/978-3-319-20615-8_15

Automating change of representation for proofs in discrete mathematics

Daniel Raggi (Lead / Corresponding author), Alan Bundy, Gudmund Grov, Alison Pease

Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

Representation determines how we can reason about a specific problem. Sometimes one representation helps us find a proof more easily than others. Most current automated reasoning tools focus on reasoning within one representation. There is, therefore, a need for the development of better tools to mechanise and automate formal and logically sound changes of representation.
In this paper we look at examples of representational transformations in discrete mathematics, and show how we have used Isabelle’s Transfer tool to automate the use of these transformations in proofs. We give a brief overview of a general theory of transformations that we consider appropriate for thinking about the matter, and we explain how it relates to the Transfer package. We show our progress towards developing a general tactic that incorporates the automatic search for representation within the proving process.

Original language	English
Title of host publication	Intelligent Computer Mathematics
Subtitle of host publication	International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015 Proceedings
Editors	Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florain Rabe, Volker Sorge
Publisher	Springer
Pages	227-242
Number of pages	16
Volume	LNAI 9150
ISBN (Electronic)	978-3-319-20615-8
ISBN (Print)	978-3-319-20614-1
DOIs	https://doi.org/10.1007/978-3-319-20615-8_15
Publication status	Published - 23 Jun 2015
Event	Conference on Intelligent Computer Mathematics - Washington, DC, United States Duration: 13 Jul 2015 → 17 Jul 2015 http://cicm-conference.org/2015/cicm.php?event=&menu=general

Publication series

Name	Lecture Notes In Computer Science
Publisher	Springer
Volume	9150
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	Conference on Intelligent Computer Mathematics
Abbreviated title	CICM 2015
Country/Territory	United States
City	Washington, DC
Period	13/07/15 → 17/07/15
Internet address	http://cicm-conference.org/2015/cicm.php?event=&menu=general

Access to Document

10.1007/978-3-319-20615-8_15

http://link.springer.com/chapter/10.1007%2F978-3-319-20615-8_15

Pease, Alison
- Computing - Senior Lecturer (Teaching and Research)
Person: Academic

Cite this

Raggi, D., Bundy, A., Grov, G., & Pease, A. (2015). Automating change of representation for proofs in discrete mathematics. In M. Kerber, J. Carette, C. Kaliszyk, F. Rabe, & V. Sorge (Eds.), Intelligent Computer Mathematics: International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015 Proceedings (Vol. LNAI 9150, pp. 227-242). (Lecture Notes In Computer Science; Vol. 9150). Springer . https://doi.org/10.1007/978-3-319-20615-8_15

Raggi, Daniel ; Bundy, Alan ; Grov, Gudmund et al. / Automating change of representation for proofs in discrete mathematics. Intelligent Computer Mathematics: International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015 Proceedings. editor / Manfred Kerber ; Jacques Carette ; Cezary Kaliszyk ; Florain Rabe ; Volker Sorge. Vol. LNAI 9150 Springer , 2015. pp. 227-242 (Lecture Notes In Computer Science).

@inproceedings{d5cae3a470d14101b33aac1225f20701,

title = "Automating change of representation for proofs in discrete mathematics",

abstract = "Representation determines how we can reason about a specific problem. Sometimes one representation helps us find a proof more easily than others. Most current automated reasoning tools focus on reasoning within one representation. There is, therefore, a need for the development of better tools to mechanise and automate formal and logically sound changes of representation.In this paper we look at examples of representational transformations in discrete mathematics, and show how we have used Isabelle{\textquoteright}s Transfer tool to automate the use of these transformations in proofs. We give a brief overview of a general theory of transformations that we consider appropriate for thinking about the matter, and we explain how it relates to the Transfer package. We show our progress towards developing a general tactic that incorporates the automatic search for representation within the proving process.",

author = "Daniel Raggi and Alan Bundy and Gudmund Grov and Alison Pease",

year = "2015",

month = jun,

day = "23",

doi = "10.1007/978-3-319-20615-8_15",

language = "English",

isbn = "978-3-319-20614-1",

volume = "LNAI 9150",

series = "Lecture Notes In Computer Science",

publisher = "Springer ",

pages = "227--242",

editor = "Manfred Kerber and Jacques Carette and Cezary Kaliszyk and Florain Rabe and Volker Sorge",

booktitle = "Intelligent Computer Mathematics",

note = "Conference on Intelligent Computer Mathematics, CICM 2015 ; Conference date: 13-07-2015 Through 17-07-2015",

url = "http://cicm-conference.org/2015/cicm.php?event=&menu=general",

}

Raggi, D, Bundy, A, Grov, G & Pease, A 2015, Automating change of representation for proofs in discrete mathematics. in M Kerber, J Carette, C Kaliszyk, F Rabe & V Sorge (eds), Intelligent Computer Mathematics: International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015 Proceedings. vol. LNAI 9150, Lecture Notes In Computer Science, vol. 9150, Springer , pp. 227-242, Conference on Intelligent Computer Mathematics, Washington, DC, United States, 13/07/15. https://doi.org/10.1007/978-3-319-20615-8_15

Automating change of representation for proofs in discrete mathematics. / Raggi, Daniel (Lead / Corresponding author); Bundy, Alan; Grov, Gudmund et al.
Intelligent Computer Mathematics: International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015 Proceedings. ed. / Manfred Kerber; Jacques Carette; Cezary Kaliszyk; Florain Rabe; Volker Sorge. Vol. LNAI 9150 Springer , 2015. p. 227-242 (Lecture Notes In Computer Science; Vol. 9150).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Automating change of representation for proofs in discrete mathematics

AU - Raggi, Daniel

AU - Bundy, Alan

AU - Grov, Gudmund

AU - Pease, Alison

PY - 2015/6/23

Y1 - 2015/6/23

N2 - Representation determines how we can reason about a specific problem. Sometimes one representation helps us find a proof more easily than others. Most current automated reasoning tools focus on reasoning within one representation. There is, therefore, a need for the development of better tools to mechanise and automate formal and logically sound changes of representation.In this paper we look at examples of representational transformations in discrete mathematics, and show how we have used Isabelle’s Transfer tool to automate the use of these transformations in proofs. We give a brief overview of a general theory of transformations that we consider appropriate for thinking about the matter, and we explain how it relates to the Transfer package. We show our progress towards developing a general tactic that incorporates the automatic search for representation within the proving process.

AB - Representation determines how we can reason about a specific problem. Sometimes one representation helps us find a proof more easily than others. Most current automated reasoning tools focus on reasoning within one representation. There is, therefore, a need for the development of better tools to mechanise and automate formal and logically sound changes of representation.In this paper we look at examples of representational transformations in discrete mathematics, and show how we have used Isabelle’s Transfer tool to automate the use of these transformations in proofs. We give a brief overview of a general theory of transformations that we consider appropriate for thinking about the matter, and we explain how it relates to the Transfer package. We show our progress towards developing a general tactic that incorporates the automatic search for representation within the proving process.

U2 - 10.1007/978-3-319-20615-8_15

DO - 10.1007/978-3-319-20615-8_15

M3 - Conference contribution

SN - 978-3-319-20614-1

VL - LNAI 9150

T3 - Lecture Notes In Computer Science

SP - 227

EP - 242

BT - Intelligent Computer Mathematics

A2 - Kerber, Manfred

A2 - Carette, Jacques

A2 - Kaliszyk, Cezary

A2 - Rabe, Florain

A2 - Sorge, Volker

PB - Springer

T2 - Conference on Intelligent Computer Mathematics

Y2 - 13 July 2015 through 17 July 2015

ER -

Raggi D, Bundy A, Grov G, Pease A. Automating change of representation for proofs in discrete mathematics. In Kerber M, Carette J, Kaliszyk C, Rabe F, Sorge V, editors, Intelligent Computer Mathematics: International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015 Proceedings. Vol. LNAI 9150. Springer . 2015. p. 227-242. (Lecture Notes In Computer Science). doi: 10.1007/978-3-319-20615-8_15

Automating change of representation for proofs in discrete mathematics

Abstract

Publication series

Conference

Access to Document

Fingerprint

Profiles

Pease, Alison

Cite this