EasyChair Publications
Search
Paper Information
Paper:Steffen Juilf Smolka and Jasmin Christian Blanchette
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs
Title:Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs
Authors:Steffen Juilf Smolka and Jasmin Christian Blanchette
Keyphrases:proof assistants, automatic theorem provers, structured proofs, skolemization, isabelle/hol, sledgehammer, higher order logic, simple type theory
Paper:
Abstract:Sledgehammer integrates external automatic theorem provers (ATPs) in the Isabelle/HOL proof assistant. To guard against bugs, ATP proofs must be reconstructed in Isabelle. Reconstructing complex proofs involves translating them to detailed Isabelle proof texts, using suitable proof methods to justify the inferences. This has been attempted before with little success, but we have addressed the main issues: Sledgehammer now transforms the proofs by contradiction into direct proofs (as described in a companion paper); it reconstructs skolemization inferences; it provides the right amount of type annotations to ensure formulas are parsed correctly without overwhelming them with types; and it iteratively tests and compresses the output, resulting in simpler and faster proofs.
Volume:Jasmin Christian Blanchette and Josef Urban (editors). PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Series:EPiC Series in Computing
Volume number:14
Pages:117-132
Editors:Jasmin Christian Blanchette and Josef Urban
Page views:10
Downloads:19
BibTeX entry:
@inproceedings{PxTP2013:Robust_Semi-Intelligible_Isabelle_Proofs_from_ATP_Proofs,
  author    = {Steffen Juilf Smolka and Jasmin Christian Blanchette},
  title     = {Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs},
  booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
  editor    = {Jasmin Christian Blanchette and Josef Urban},
  series    = {EPiC Series in Computing},
  volume    = {14},
  pages     = {117-132},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}