Compression of Propositional Resolution Proofs via Partial Regularization

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 : 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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00617846
Contributor : Pascal Fontaine <>
Submitted on : Tuesday, August 30, 2011 - 3:58:15 PM
Last modification on : Thursday, February 21, 2019 - 2:02:02 PM

Links full text

Identifiers

Collections

Citation

Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo. Compression of Propositional Resolution Proofs via Partial Regularization. 23rd International Conference on Automated Deduction - CADE-23, Jul 2011, Wroclaw, Poland. pp.237-251, ⟨10.1007/978-3-642-22438-6_19⟩. ⟨inria-00617846⟩

Share

Metrics

Record views

157