Skip to Main content Skip to Navigation
Journal articles

Scalable Fine-Grained Proofs for Formula Processing

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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [48 references]  Display  Hide  Download

https://hal.inria.fr/hal-02515103
Contributor : Jasmin Blanchette <>
Submitted on : Monday, March 23, 2020 - 11:53:29 AM
Last modification on : Thursday, April 30, 2020 - 10:04:14 PM
Document(s) archivé(s) le : Wednesday, June 24, 2020 - 2:05:19 PM

File

processing_article.pdf
Files produced by the author(s)

Identifiers

Citation

Haniel Barbosa, Jasmin Blanchette, Mathias Fleury, Pascal Fontaine. Scalable Fine-Grained Proofs for Formula Processing. Journal of Automated Reasoning, Springer Verlag, 2020, 64 (3), pp.485-510. ⟨10.1007/s10817-018-09502-y⟩. ⟨hal-02515103⟩

Share

Metrics

Record views

202

Files downloads

628