Skip to Main content Skip to Navigation
New interface
Conference papers

Exploring and Exploiting Algebraic and Graphical Properties of Resolution

Pascal Fontaine 1 Stephan Merz 1 Bruno Woltzenlogel Paleo 1 
1 VERIDIS - VERIfication pour les systèmes DIStribués
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications : UMR7503
Abstract : Integrating an SMT solver in a certified environment such as an LF-style proof assistant requires the solver to output proofs. Unfortunately, those proofs may be quite large, and the overhead of rechecking the proof may account for a significant fraction of the proof time. In this paper we explore techniques for reducing the sizes of propositional proofs, which are at the core of SMT proofs. Our techniques are justified in an algebra of resolution and rely on a graph-theoretical representation of proofs that allows us to detect the potential for reordering and combining resolution inferences.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Bruno Woltzenlogel Paleo Connect in order to contact the contributor
Submitted on : Saturday, December 11, 2010 - 8:48:45 PM
Last modification on : Friday, February 4, 2022 - 3:33:14 AM
Long-term archiving on: : Monday, November 5, 2012 - 1:16:25 PM


Files produced by the author(s)


  • HAL Id : inria-00544658, version 1



Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo. Exploring and Exploiting Algebraic and Graphical Properties of Resolution. 8th International Workshop on Satisfiability Modulo Theories - SMT 2010, Jul 2010, Edinburgh, United Kingdom. ⟨inria-00544658⟩



Record views


Files downloads