Scalable Fine-Grained Proofs for Formula Processing

Haniel Barbosa 1, 2, 3 Jasmin Blanchette 3, 4 Pascal Fontaine 1, 3
1 UL - Université de Lorraine
2 UFRN - Universidade Federal do Rio Grande do Norte [Natal]
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
4 MPII - Max-Planck-Institut für Informatik
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.
Keywords : proof production proof checking satisfiability modulo theories automatic theorem proving
Type de document :
Rapport
[Research Report] Universite de Lorraine, CNRS, Inria, LORIA, Nancy, France; Universidade Federal do Rio Grande do Norte, Natal, Brazil; Vrije Universiteit Amsterdam, Amsterdam, The Netherlands; Max-Planck-Institut für Informatik, Saarbrücken, Germany. 2017, pp.25
Liste complète des métadonnées

Littérature citée [42 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01526841
Contributeur : Haniel Barbosa <>
Soumis le : mardi 23 mai 2017 - 15:42:40
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13
Document(s) archivé(s) le : lundi 28 août 2017 - 17:51:13

Fichier

rep.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01526841, version 1

Collections

INRIA | LORIA | LORIA-FM | LARA | UNIV-LORRAINE | INRIA2017 | GRID5000

Citation

Haniel Barbosa, Jasmin Blanchette, Pascal Fontaine. Scalable Fine-Grained Proofs for Formula Processing. [Research Report] Universite de Lorraine, CNRS, Inria, LORIA, Nancy, France; Universidade Federal do Rio Grande do Norte, Natal, Brazil; Vrije Universiteit Amsterdam, Amsterdam, The Netherlands; Max-Planck-Institut für Informatik, Saarbrücken, Germany. 2017, pp.25. 〈hal-01526841〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

188

Téléchargements de fichiers

44

Contact


archive-ouverte@inria.fr