[Back]

B. Woltzenlogel-Paleo:
"Compression of Propositional Resolution Proofs";
Talk: 2nd Workshop Structural Proof Theory, Innsbruck (invited); 2011-10-26 - 2011-10-29.

In this talk two methods for the compression of propositional
resolution proofs will be explained and illustrated in detail.
The first method is based on removing irregularities from the proof.
The second method consists of moving downward resolution inferences
with unit clauses as their premises.
Experimental results obtained by applying these methods on proofs
output by a sat-solver on standard benchmarks of the sat-lib and the
sat-race competition will also be shown.

In this talk two methods for the compression of propositional
resolution proofs will be explained and illustrated in detail.
The first method is based on removing irregularities from the proof.
The second method consists of moving downward resolution inferences
with unit clauses as their premises.
Experimental results obtained by applying these methods on proofs
output by a sat-solver on standard benchmarks of the sat-lib and the
sat-race competition will also be shown.

Resolution, Proof Compression, Proof Theory, Logic, Propositional Logic