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.
References: