Automating Change of Representation for Proofs in Discrete Mathematics

Daniel Raggi, Alan Bundy, Gudmund Grov, Alison Pease

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationIntelligent Computer Mathematics
Subtitle of host publicationInternational Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings.
EditorsManfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, Volker Sorge
PublisherSpringer
Pages227-242
Number of pages16
ISBN (Electronic)978-3-319-20615-8
ISBN (Print)978-3-319-20614-1
DOIs
Publication statusPublished - 2015
EventInternational Conference on Intelligent Computer Mathematics 2015 - Washington, United States
Duration: 13 Jul 201517 Jul 2015

Publication series

NameLecture Notes in Computer Science
Volume9150
ISSN (Print)0302-9743

Conference

ConferenceInternational Conference on Intelligent Computer Mathematics 2015
Abbreviated titleCICM 2015
CountryUnited States
CityWashington
Period13/07/1517/07/15

Keywords

  • Change of representation
  • Transformation
  • Automated reasoning
  • Isabelle proof assistant

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. (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 ; Pease, Alison. / 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 ; Florian Rabe ; Volker Sorge. Springer, 2015. pp. 227-242 (Lecture Notes in Computer Science).
@inproceedings{34e82b590ad8483cb5afee5a44f1c3f3,
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'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.",
keywords = "Change of representation, Transformation, Automated reasoning, Isabelle proof assistant",
author = "Daniel Raggi and Alan Bundy and Gudmund Grov and Alison Pease",
year = "2015",
doi = "10.1007/978-3-319-20615-8_15",
language = "English",
isbn = "978-3-319-20614-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "227--242",
editor = "Manfred Kerber and Jacques Carette and Cezary Kaliszyk and Florian Rabe and Volker Sorge",
booktitle = "Intelligent Computer Mathematics",

}

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.. Lecture Notes in Computer Science, vol. 9150, Springer, pp. 227-242, International Conference on Intelligent Computer Mathematics 2015, Washington, 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; Bundy, Alan; Grov, Gudmund; Pease, Alison.

Intelligent Computer Mathematics: International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings.. ed. / Manfred Kerber; Jacques Carette; Cezary Kaliszyk; Florian Rabe; Volker Sorge. Springer, 2015. p. 227-242 (Lecture Notes in Computer Science; Vol. 9150).

Research output: Chapter in Book/Report/Conference proceedingConference 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

Y1 - 2015

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.

KW - Change of representation

KW - Transformation

KW - Automated reasoning

KW - Isabelle proof assistant

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

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, Florian

A2 - Sorge, Volker

PB - Springer

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.. Springer. 2015. p. 227-242. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-20615-8_15