Sciweavers

Share
JAR
2016

Semi-intelligible Isar Proofs from Machine-Generated Proofs

4 years 3 months ago
Semi-intelligible Isar Proofs from Machine-Generated Proofs
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 Isabelle. 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. Keywords Automatic theorem provers · Proof assistants · Natural deduction
Jasmin Christian Blanchette, Sascha Böhme, Ma
Added 06 Apr 2016
Updated 06 Apr 2016
Type Journal
Year 2016
Where JAR
Authors Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier
Comments (0)
books