Semi-intelligible Isar Proofs from Machine-Generated Proofs

J.C. Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, Albert Steckermeier

Research output: Contribution to JournalArticleAcademicpeer-review

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 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.
Original languageEnglish
Pages (from-to)155-200
JournalJournal of Automated Reasoning
DOIs
Publication statusPublished - 2016
Externally publishedYes

Cite this