Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS/CISA Joint Seminar: Stefan Hetzl

LFCS/CISA Joint Seminar: Stefan Hetzl

— filed under:

Algorithmic Introduction of Quantified Cuts

  • LFCS Seminar
When May 06, 2013
from 02:00 PM to 03:00 PM
Where IF 2.33
Add event to calendar vCal



We describe proof-theoretic results on cut-elimination in classical first-order logic and show how they lead to a method for abbreviating a cut-free proof by the introduction of lemmas.

The cut-introduction algorithm works by first computing a compressed representation of the terms present in the cut-free proof and then formulas that realize such a compression. Finally, a proof using these formulas as lemmas is constructed.

This method allows an exponential compression of proof length. A prototype implementation is available on the web and will be demonstrated briefly during this talk.

Document Actions