TY - JOUR
T1 - Semi-intelligible Isar Proofs from Machine-Generated Proofs
AU - Blanchette, J.C.
AU - Böhme, Sascha
AU - Fleury, Mathias
AU - Smolka, Steffen Juilf
AU - Steckermeier, Albert
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
U2 - 10.1007/s10817-015-9335-3
DO - 10.1007/s10817-015-9335-3
M3 - Article
SN - 0168-7433
SP - 155
EP - 200
JO - Journal of Automated Reasoning
JF - Journal of Automated Reasoning
ER -