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 metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/inria-00544658
Contributor : Bruno Woltzenlogel Paleo <>
Submitted on : Saturday, December 11, 2010 - 8:48:45 PM
Last modification on : Thursday, February 21, 2019 - 2:02:02 PM
Long-term archiving on : Monday, November 5, 2012 - 1:16:25 PM

File

AlgebraicPropertiesOfResolutio...
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00544658, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

245

Files downloads

136