Scalable fine-grained proofs for formula processing

Haniel Barbosa*, Jasmin Christian Blanchette, Pascal Fontaine

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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

Original languageEnglish
Title of host publicationAutomated Deduction -CADE 26
Subtitle of host publication26th International Conference on Automated Deduction, Proceedings
EditorsLeonardo de Moura
PublisherSpringer/Verlag
Pages398-412
Number of pages15
ISBN (Electronic) 9783319630465
ISBN (Print)9783319630458
DOIs
Publication statusPublished - 2017
Event26th International Conference on Automated Deduction, CADE-26 2017 - Gothenburg, Sweden
Duration: 6 Aug 201711 Aug 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10395 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th International Conference on Automated Deduction, CADE-26 2017
Country/TerritorySweden
CityGothenburg
Period6/08/1711/08/17

Funding

We thank Simon Cruanes for discussing many aspects of the framework with us as it was emerging, and we thank Robert Lewis, Stephan Merz, Lawrence Paulson, Anders Schlichtkrull, Mark Summerfield, Sophie Tourret, and the anonymous reviewers for suggesting many textual improvements. This research has been partially supported by the Agence nationale de la recherche/Deutsche Forschungsgemeinschaft project SMArT (ANR-13-IS02-0001, STU 483/2-1) and by the European Union project SC2 (grant agreementNo. 712689).Thework has also received funding from theEuropean Research Council under the European Union?sHorizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Experiments presented in this paper 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 aswell as other organizations.Amirror of all the software and evaluation data described in this paper is hosted by Zenodo (https://doi.org/10.5281/zenodo.582482).

FundersFunder number
Agence nationale de la recherche/Deutsche ForschungsgemeinschaftANR-13-IS02-0001, STU 483/2-1
Horizon 2020 Framework Programme713999, 712689
European Commission
European Research Council

    Fingerprint

    Dive into the research topics of 'Scalable fine-grained proofs for formula processing'. Together they form a unique fingerprint.

    Cite this