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

DOI10.1007/S11786-016-0275-ZzbMATH Open1409.68261OpenAlexW2417291013WikidataQ59474485 ScholiaQ59474485MaRDI QIDQ2364883FDOQ2364883

Authors: Daniel Raggi, Alan Bundy, Gudmund Grov, 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

Recommendations

• Automating Change of Representation for Proofs in Discrete Mathematics
• Changing data representation within the \textsf{Coq} system
• The interaction of representation and reasoning
• scientific article; zbMATH DE number 2085174
• scientific article; zbMATH DE number 1954188

zbMATH Keywords

transformationautomated reasoningIsabelle proof assistantchange of representation

Mathematics Subject Classification ID

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

Cites Work

• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• IMPS: An interactive mathematical proof system
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• A course in combinatorics.
• Isabelle/HOL. A proof assistant for higher-order logic
• Institutions: abstract model theory for specification and programming
• Translating higher-order clauses to first-order clauses
• HOL with definitions: semantics, soundness, and a verified implementation
• A new look at generalized rewriting in type theory
• Sledgehammer: judgement day
• A walk through combinatorics. An introduction to enumeration and graph theory
• Constructive Type Classes in Isabelle
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• Data refinement in Isabelle/HOL
• A Consistent Foundation for Isabelle/HOL
• Using tactics to reformulate formulae for resolution theorem proving
• The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof

Cited In (4)

• Changing data representation within the \textsf{Coq} system
• Automating Change of Representation for Proofs in Discrete Mathematics
• Can an A.I. win a medal in the mathematical olympiad? – Benchmarking mechanized mathematics on pre-university problems1
• Title not available (Why is that?)

Uses Software

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

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

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