Discovery - University of Dundee - Online Publications

Library & Learning Centre

Automating Change of Representation for Proofs in Discrete Mathematics (Extended Version)

Automating Change of Representation for Proofs in Discrete Mathematics (Extended Version)

Research output: Contribution to journalArticle

View graph of relations


  • Daniel Raggi (Lead / Corresponding author)
  • Alan Bundy
  • Gudmund Grov
  • Alison Pease

Research units


Original languageEnglish
Pages (from-to)1-29
Number of pages29
JournalMathematics in Computer Science
Issue number4
Early online date18 Jul 2016
StatePublished - Dec 2016


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.

Download statistics

No data available


Open Access permissions



  • Final Published Version

    Final published version, 733 KB, PDF-document

    © The Author(s) 2016. This article is distributed under the terms of the Creative Commons Attribution 4.0 International License
    (, which permits unrestricted use, distribution, and reproduction in any medium, provided
    you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if
    changes were made.


Library & Learning Centre

Contact | Accessibility | Policy