## 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.

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

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 |