Semi-intelligible Isar Proofs from Machine-Generated Proofs - Archive ouverte HAL Access content directly
Journal Articles Journal of Automated Reasoning Year : 2016

Semi-intelligible Isar Proofs from Machine-Generated Proofs

(1, 2, 3) , (4) , (2, 5) , (6) , (4)
1
2
3
4
5
6

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.
Fichier principal
Vignette du fichier
paper.pdf (459.25 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01211748 , version 1 (05-10-2015)

Identifiers

Cite

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, 2016, ⟨10.1007/s10817-015-9335-3⟩. ⟨hal-01211748⟩
259 View
267 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More