Techniques for proof compression

Bruno Woltzenlogel Paleo

Fakultät für Informatik
Technische Universität Wien

Thursday, 27 June 2013, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf], [mov]

Abstract: This talk will provide an overview of algorithms for compressing formal proofs.

For propositional resolution proofs, the focus will be on efficient algorithms for (partial) regularization (i.e. removal of redundant proof nodes obtained by resolution inferences that use a resolved atom that has already been used elsewhere in the proof) [1][2]. Experimental results on several proofs produced by the SMT-solver VeriT will be discussed.

For natural deduction proofs, a calculus that extends the usual natural deduction calculus by allowing inferences rules to operate directly on subformulas within contexts will be presented. In this extended calculus, proofs can be quadratically smaller [3].

The techniques presented in this talk have open-source implementations in the Skeptik framework.


  1. "Compression of Propositional Resolution Proofs via Partial Regularization" (CADE 2011)
  2. "Compression of Propositional Resolution Proofs by Lowering Subproofs" (TABLEAUX 2013)
  3. "Contextual Natural Deduction" (LFCS 2013)

Tarmo Uustalu
Last update 8.7.2013