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)1-26
Number of pages26
JournalJournal of Automated Reasoning
DOIs
Publication statusE-pub ahead of print - 4 Jan 2019

Fingerprint

Surface mount technology
Data structures
Processing

Keywords

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

Cite this

Barbosa, Haniel ; Blanchette, Jasmin Christian ; Fleury, Mathias ; Fontaine, Pascal. / Scalable Fine-Grained Proofs for Formula Processing. In: Journal of Automated Reasoning. 2019 ; pp. 1-26.
@article{6a3c1cf57057425991af94efefebd1c9,
title = "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.",
keywords = "Formula processing, Proof checking, Proof production, Proof reconstruction, Rewriting, SMT",
author = "Haniel Barbosa and Blanchette, {Jasmin Christian} and Mathias Fleury and Pascal Fontaine",
year = "2019",
month = "1",
day = "4",
doi = "10.1007/s10817-018-09502-y",
language = "English",
pages = "1--26",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",

}

Scalable Fine-Grained Proofs for Formula Processing. / Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal.

In: Journal of Automated Reasoning, 04.01.2019, p. 1-26.

Research output: Contribution to JournalArticleAcademicpeer-review

TY - JOUR

T1 - Scalable Fine-Grained Proofs for Formula Processing

AU - Barbosa, Haniel

AU - Blanchette, Jasmin Christian

AU - Fleury, Mathias

AU - Fontaine, Pascal

PY - 2019/1/4

Y1 - 2019/1/4

N2 - 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.

AB - 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.

KW - Formula processing

KW - Proof checking

KW - Proof production

KW - Proof reconstruction

KW - Rewriting

KW - SMT

UR - http://www.scopus.com/inward/record.url?scp=85059666689&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85059666689&partnerID=8YFLogxK

U2 - 10.1007/s10817-018-09502-y

DO - 10.1007/s10817-018-09502-y

M3 - Article

SP - 1

EP - 26

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

ER -