Paper Info
Title
Automating Change of Representation for Proofs in Discrete Mathematics (Extended Version).
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.
Year
DOI
Venue
2016
10.1007/s11786-016-0275-z
Mathematics in Computer Science
Keywords
Field
DocType
Change of representation, Transformation, Automated reasoning, Isabelle proof assistant, 68T15 Theorem proving (deduction, resolution, etc.), 68T20 Problem solving (heuristics, search strategies, etc.), 68T27 Logic in artificial intelligence, 68T30 Knowledge representation, 68R01 General (discrete mathematics in relation to computer science), 03B35 Mechanization of proofs and logical operations
Discrete mathematics,Automated reasoning,Programming language,Computer science,Automation,Theoretical computer science,Mathematical proof
Journal
Volume
Issue
ISSN
10
4
1661-8270
Citations 
PageRank 
References 
1
0.43
8
Authors
4
Name
Order
Citations
PageRank
Daniel Raggi110.77
A. Bundy23713532.03
Gudmund Grov310017.38
Alison Pease414517.82