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

223 Downloads (Pure)

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
Number of pages26
JournalJournal of Automated Reasoning
Volume64
Issue number3
Early online date4 Jan 2019
DOIs
Publication statusPublished - 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).

FundersFunder number
RENATER
Horizon 2020 Framework Programme713999, 712689
College of Natural Resources and Sciences, Humboldt State University
European Research Council

    Keywords

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

    Fingerprint

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

    Cite this