Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais,
"Reconstruction of Fine-Grained Proofs in a Proof Assistant"
: CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, Springer, Seite(n) 450, 7-2021, ISBN: 978-3-030-79876-5
Reconstruction of Fine-Grained Proofs in a Proof Assistant
Sprache des Titels:
CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings
We present a fast and reliable reconstruction of proofs gener-ated by the SMT solver veriT in Isabelle. The fine-grained proof formatmakes the reconstruction simple and efficient. For typical proof steps,such as arithmetic reasoning and skolemization, our reconstruction canavoid expensive search. By skipping proof steps that are irrelevant forIsabelle, the performance of proof checking is improved. Our methodincreases the success rate of Sledgehammer by halving the failure rateand reduces the checking time by 13%. We provide a detailed evaluationof the reconstruction time for each rule. The runtime is influenced byboth simple rules that appear very often and common complex rules