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.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2016, 〈10.1007/s10817-015-9335-3〉
Liste complète des métadonnées

Littérature citée [82 références]  Voir  Masquer  Télécharger
Contributeur : Jasmin Christian Blanchette <>
Soumis le : lundi 5 octobre 2015 - 16:30:54
Dernière modification le : mardi 18 décembre 2018 - 16:38:25
Document(s) archivé(s) le : mercredi 6 janvier 2016 - 10:46:07


Fichiers produits par l'(les) auteur(s)




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〉



Consultations de la notice


Téléchargements de fichiers