Scalable Fine-Grained Proofs for Formula Processing

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

Research output: Contribution to JournalArticleAcademicpeer-review

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 languageEnglish
Pages (from-to)485-510
JournalJournal of Automated Reasoning
Volume64
Issue number3
DOIs
Publication statusPublished - Mar 2020

Keywords

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

Cite this