Reconstructing veriT Proofs in Isabelle/HOL
Mathias Fleury (Max Planck Institut for Informatics), Hans-J\"org, Schurr (University of Lorraine, CNRS, Inria, and LORIA)
TL;DR
This paper presents a reconstruction method in Isabelle/HOL for proofs generated by the veriT SMT solver, enhancing trustworthiness and integrating automated proofs into interactive theorem proving.
Contribution
It introduces an improved reconstruction procedure for veriT proofs within Isabelle/HOL, addressing design challenges and demonstrating practical effectiveness.
Findings
veriT proofs can be reliably reconstructed in Isabelle/HOL
the veriT-powered smt tactic is often the fastest proof method
the approach enhances proof trustworthiness and automation
Abstract
Automated theorem provers are now commonly used within interactive theorem provers to discharge an increasingly large number of proof obligations. To maintain the trustworthiness of a proof, the automatically found proof must be verified inside the proof assistant. We present here a reconstruction procedure in the proof assistant Isabelle/HOL for proofs generated by the satisfiability modulo theories solver veriT which is part of the smt tactic. We describe in detail the architecture of our improved reconstruction method and the challenges we faced in designing it. Our experiments show that the veriT-powered smt tactic is regularly suggested by Sledgehammer as the fastest method to automatically solve proof goals.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.