Projects per year
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 1317, 2015, Proceedings. 
Publisher  Springer International Publishing 
Pages  227242 
Number of pages  16 
ISBN (Electronic)  9783319206158 
ISBN (Print)  9783319206141 
DOIs  
Publication status  Published  2015 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer International Publishing 
Volume  9150 
ISSN (Print)  03029743 
ISSN (Electronic)  16113349 
Projects
 2 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

The integration and interaction of multiple mathematical reasoning processes
Bundy, A., Aspinall, D., Fleuriot, J., Jackson, P., Smaill, A., Colton, S., Ireland, A. & Michaelson, G.
1/08/11 → 31/07/15
Project: Research