Compression of Propositional Resolution Proofs via Partial Regularization

Pascal Fontaine 1, 2 Stephan Merz 1, 2 Bruno Woltzenlogel Paleo 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper describes two algorithms for the compression of propositional resolution proofs. The first algorithm performs partial regularization, removing an inference $\eta$ when it is redundant in the sense that its pivot literal already occurs as the pivot of another inference located below in the path from $\eta$ to the root of the proof. The second algorithm delays the resolution of (both input and derived) unit clauses, thus removing (some) inferences having the same pivot but possibly occurring also in different branches of the proof.
Type de document :
Communication dans un congrès
Nikolaj Bjrner and Viorica Sofronie-Stokkermans. 23rd International Conference on Automated Deduction - CADE-23, Jul 2011, Wroclaw, Poland. Springer, 6803, pp.237-251, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-22438-6_19〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00617846
Contributeur : Pascal Fontaine <>
Soumis le : mardi 30 août 2011 - 15:58:15
Dernière modification le : jeudi 11 janvier 2018 - 06:23:25

Lien texte intégral

Identifiants

Collections

Citation

Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo. Compression of Propositional Resolution Proofs via Partial Regularization. Nikolaj Bjrner and Viorica Sofronie-Stokkermans. 23rd International Conference on Automated Deduction - CADE-23, Jul 2011, Wroclaw, Poland. Springer, 6803, pp.237-251, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-22438-6_19〉. 〈inria-00617846〉

Partager

Métriques

Consultations de la notice

126