Abstract: Reliable Reconstruction of Fine-Grained
Proofs in a Proof Assistant
Hans-Jörg Schurr1 , Mathias Fleury2,3 and Martin Desharnais4
1
  University of Lorraine, CNRS, Inria, and LORIA, Nancy, France
2
  Johannes Kepler University Linz, Linz, Austria
3
  Max-Planck Institute für Informatik, Saarland Informatics Campus, Saarbrücken, Germany
4
  Universität der Bundeswehr München, München, Germany


                                         Abstract
                                         We present a fast and reliable reconstruction of proofs generated 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. This work was
                                         originally presented at CADE 28.

                                         Keywords
                                         automatic theorem provers, proof assistants, proof verification




SMT’21: 19th International Workshop on Satisfiability Modulo Theories, July 18–19, 2021, Online
" hans-jorg.schurr@inria.fr (H. Schurr); mathias.fleury@jku.at (M. Fleury); martin.desharnais@unibw.de
(M. Desharnais)
 0000-0002-0829-5056 (H. Schurr); 0000-0002-1705-3083 (M. Fleury); 0000-0002-1830-7532 (M. Desharnais)
                                       © 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073       CEUR Workshop Proceedings (CEUR-WS.org)



                                                                                                          64