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


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
Subtitle of host publicationCADE 26 - 26th International Conference on Automated Deduction, Proceedings
EditorsLeonardo de Moura
Number of pages15
ISBN (Electronic) 9783319630465
ISBN (Print)9783319630458
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


Conference26th International Conference on Automated Deduction, CADE-26 2017


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

Cite this