Abstract
We present a framework for processing formulas in automatic theorem provers, with generation of detailed proofs. The main components are a generic contextual recursion algorithm and an extensible set of inference rules. Clausification, skolemization, theory-specific simplifications, and expansion of ‘let’ expressions are instances of this framework. With suitable data structures, proof generation adds only a linear-time overhead, and proofs can be checked in linear time. We implemented the approach in the SMT solver veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced, which is important for independent checking and reconstruction in proof assistants. To validate the framework, we implemented proof reconstruction in Isabelle/HOL.
Original language | English |
---|---|
Pages (from-to) | 485-510 |
Number of pages | 26 |
Journal | Journal of Automated Reasoning |
Volume | 64 |
Issue number | 3 |
Early online date | 4 Jan 2019 |
DOIs | |
Publication status | Published - Mar 2020 |
Funding
We thank Simon Cruanes for discussing many aspects of the framework with us as it was emerging. We also thank Robert Lewis, Stephan Merz, Lawrence Paulson, Anders Schlichtkrull, Hans-Jörg Schurr, Mark Summerfield, Sophie Tourret, and the anonymous reviewers for suggesting many improvements. The work has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (Grant Agreement No. 713999, Matryoshka). Experiments presented in this article were carried out using the Grid’5000 testbed (https://www.grid5000.fr/), supported by a scientific interest group hosted by Inria and including CNRS, RENATER, and several universities as well as other organizations. A mirror of all the software and evaluation data described in this article is hosted by Zenodo (https://doi.org/10.5281/zenodo.582482).
Funders | Funder number |
---|---|
RENATER | |
Horizon 2020 Framework Programme | 713999, 712689 |
College of Natural Resources and Sciences, Humboldt State University | |
European Research Council |
Keywords
- Formula processing
- Proof checking
- Proof production
- Proof reconstruction
- Rewriting
- SMT