Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais,
"Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant"
, in André Platzer and Geoff Sutcliffe: In Automated Deduction - CADE 28, Serie 28th International Conference on Automated Deduction Conference Paper, Springer, 7-2021
Original Titel:
Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant
Sprache des Titels:
Englisch
Original Buchtitel:
In Automated Deduction - CADE 28
Original Kurzfassung:
We present a fast and reliable reconstruction of proofs gener-
ated by the SMT solver veriT in Isabelle. The fine-grained proof format
makes the reconstruction simple and efficient. For typical proof steps,
such as arithmetic reasoning and skolemization, our reconstruction can
avoid expensive search. By skipping proof steps that are irrelevant for
Isabelle, the performance of proof checking is improved. Our method
increases the success rate of Sledgehammer by halving the failure rate
and reduces the checking time by 13%. We provide a detailed evaluation
of the reconstruction time for each rule. The runtime is influenced by
both simple rules that appear very often and common complex rules.
Sprache der Kurzfassung:
Englisch
Veröffentlicher:
Springer
Serie:
28th International Conference on Automated Deduction Conference Paper