Automating change of representation for proofs in discrete mathematics (extended version)

DOI10.1007/s11786-016-0275-zzbMath1409.68261OpenAlexW2417291013WikidataQ59474485 ScholiaQ59474485MaRDI QIDQ2364883

Daniel Raggi, Gudmund Grov, Alan Bundy, Alison Pease

Publication date: 25 July 2017

Published in: Mathematics in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11786-016-0275-z

zbMATH Keywords

automated reasoningtransformationIsabelle proof assistantchange of representation

Mathematics Subject Classification ID

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

Related Items (1)

Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• IMPS: An interactive mathematical proof system
• Using tactics to reformulate formulae for resolution theorem proving
• Isabelle/HOL. A proof assistant for higher-order logic
• Translating higher-order clauses to first-order clauses
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• A Consistent Foundation for Isabelle/HOL
• Constructive Type Classes in Isabelle
• Institutions: abstract model theory for specification and programming
• The New Quickcheck for Isabelle
• Data Refinement in Isabelle/HOL
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
• Sledgehammer: Judgement Day
• Interpretation of Locales in Isabelle: Theories and Proof Contexts

This page was built for publication: Automating change of representation for proofs in discrete mathematics (extended version)