Semi-intelligible Isar Proofs from Machine-Generated Proofs

Abstract : Sledgehammer is a component of the Isabelle/HOL proof assistant that integrates external automatic theorem provers (ATPs) to discharge interactive proof obligations. As a safeguard against bugs, the proofs found by the external provers are reconstructed in Isa-belle. Reconstructing complex arguments involves translating them to Isabelle's Isar format, supplying suitable justifications for each step. Sledgehammer transforms the proofs by contradiction into direct proofs; it iteratively tests and compresses the output, resulting in simpler and faster proofs; and it supports a wide range of ATPs, including E, LEO-II, Satallax, SPASS, Vampire, veriT, Waldmeister, and Z3.
Document type :
Journal articles
Complete list of metadatas

Cited literature [82 references]  Display  Hide  Download

https://hal.inria.fr/hal-01211748
Contributor : Jasmin Blanchette <>
Submitted on : Monday, October 5, 2015 - 4:30:54 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Long-term archiving on : Wednesday, January 6, 2016 - 10:46:07 AM

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier. Semi-intelligible Isar Proofs from Machine-Generated Proofs. Journal of Automated Reasoning, Springer Verlag, 2016, ⟨10.1007/s10817-015-9335-3⟩. ⟨hal-01211748⟩

Share

Metrics

Record views

308

Files downloads

364