Projects per year
Abstract
Representation determines how we can reason about a specific problem. Sometimes one representation helps us to 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 tools from Isabelle's Transfer package to automate the use of these transformations in proofs. We give an 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 a few reasoning tactics we developed in Isabelle to improve the use of transformations, including the automation of search in the space of representations. We present and analyse some results of the use of these tactics.
Original language  English 

Pages (fromto)  429–457 
Number of pages  29 
Journal  Mathematics in Computer Science 
Volume  10 
Issue number  4 
DOIs  
Publication status  Published  Oct 2016 
Fingerprint
Dive into the research topics of 'Automating change of representation for proofs in discrete mathematics (extended version)'. Together they form a unique fingerprint.Projects
 1 Finished

The integration and interaction of multiple mathematical Reasoning Processes
Bundy, A., Aspinall, D., Colton, S., Fleuriot, J., Gow, J., Grov, G., Ireland, A., Jackson, P., Mcneill, F., Michaelson, G. & Smaill, A.
1/11/15 → 31/10/19
Project: Research
Profiles

Alan Bundy
 School of Informatics  Professor
 Artificial Intelligence and its Applications Institute
 Data Science and Artificial Intelligence
Person: Academic: Research Active