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.
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
PB - Springer International Publishing
ER -