Scalable Fine-Grained Proofs for Formula Processing

Haniel Barbosa*, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine

*Corresponding author for this work

Research output: Contribution to JournalArticleAcademicpeer-review

187 Downloads (Pure)


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 languageEnglish
Pages (from-to)485-510
Number of pages26
JournalJournal of Automated Reasoning
Issue number3
Early online date4 Jan 2019
Publication statusPublished - Mar 2020


  • Formula processing
  • Proof checking
  • Proof production
  • Proof reconstruction
  • Rewriting
  • SMT


Dive into the research topics of 'Scalable Fine-Grained Proofs for Formula Processing'. Together they form a unique fingerprint.

Cite this