[Back]

Contributions to Proceedings:

B. Woltzenlogel-Paleo, P. Fontaine, S. Merz:
"Compression of Propositional Resolution Proofs via Partial Regularization";
in: "Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings", Springer, 2011, ISBN: 978-3-642-22437-9, 237 - 251.

English abstract:
This paper describes two algorithms for the compression
of propositional resolution proofs. The first algorithm, RecyclePivotsWithIntersection, 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, LowerUnits, delays the resolution of (both input and derived) unit clauses, thus removing
(some) inferences having the same pivot but possibly occurring also in
diff erent branches of the proof.

German abstract:
This paper describes two algorithms for the compression
of propositional resolution proofs. The first algorithm, RecyclePivotsWithIntersection, 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, LowerUnits, delays the resolution of (both input and derived) unit clauses, thus removing
(some) inferences having the same pivot but possibly occurring also in
diff erent branches of the proof.

Keywords:
Resolution, Compression, Proof Theory, Proof Compression, SAT-Solving, SMT-Solving

"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:

Created from the Publication Database of the Vienna University of Technology.