Exploring and Exploiting Algebraic and Graphical Properties of Resolution

Pascal Fontaine 1 Stephan Merz 1 Bruno Woltzenlogel Paleo 1
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Type de document :
Communication dans un congrès
8th International Workshop on Satisfiability Modulo Theories - SMT 2010, Jul 2010, Edinburgh, United Kingdom. 2010
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00544658
Contributeur : Bruno Woltzenlogel Paleo <>
Soumis le : samedi 11 décembre 2010 - 20:48:45
Dernière modification le : jeudi 11 janvier 2018 - 06:23:13
Document(s) archivé(s) le : lundi 5 novembre 2012 - 13:16:25

Fichier

AlgebraicPropertiesOfResolutio...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. 2010. 〈inria-00544658〉

Partager

Métriques

Consultations de la notice

227

Téléchargements de fichiers

119