Automating Change of Representation for Proofs in Discrete Mathematics

DOI10.1007/978-3-319-20615-8_15MaRDI QIDQ3453117zbMATH OpenOpenAlexFDO

Authors Daniel Raggi, Alan Bundy, Gudmund Grov, Alison Pease

Publication date 20 November 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1505.02449

zbMATH Keywords

automated reasoningchange of representationIsabelle proof assistanttransformation

Mathematics Subject Classification ID

General topics of discrete mathematics in relation to computer science (68R01) Logic in artificial intelligence (68T27) Knowledge representation (68T30)

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.

Recommendations

• Automating change of representation for proofs in discrete mathematics (extended version)
• scientific article; zbMATH DE number 1787153
• On automating diagrammatic proofs of arithmetic arguments
• Automated constructivization of proofs
• Proof simplification and automated theorem proving
• scientific article; zbMATH DE number 978243
• Automatic proving with disjunctive proving methods
• Automating the search for elegant proofs
• scientific article; zbMATH DE number 4078854
• Automatic Proof Generation in Kleene Algebra

Cites work

• scientific article; zbMATH DE number 1120551 (Why is no real title available?)
• IMPS: An interactive mathematical proof system
• Institutions: abstract model theory for specification and programming
• Isabelle/HOL. A proof assistant for higher-order logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder

Cited in

(5)

• A new compact finite difference quasilinearization method for nonlinear evolution partial differential equations
• Automating change of representation for proofs in discrete mathematics (extended version)
• scientific article; zbMATH DE number 2085174 (Why is no real title available?)
• The role of representations in mathematical reasoning
• A system simulating representation change phenomena while problem solving

Describes a project that uses

Uses Software

• Isabelle
• Hets
• IMPS
• Sledgehammer
• Nitpick
• Isabelle/HOL
• Transfer
• Lifting

This page was built for publication: Automating Change of Representation for Proofs in Discrete Mathematics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453117)