Scalable Fine-Grained Proofs for Formula Processing - Archive ouverte HAL Access content directly
Journal Articles Journal of Automated Reasoning Year : 2020

Scalable Fine-Grained Proofs for Formula Processing

(1) , (2, 3, 1) , (2) , (1, 4)
1
2
3
4

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.
Fichier principal
Vignette du fichier
processing_article.pdf (236.16 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02515103 , version 1 (23-03-2020)

Identifiers

Cite

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

Altmetric

Share

Gmail Facebook Twitter LinkedIn More