LFCS/CISA Joint Seminar: Stefan Hetzl
Algorithmic Introduction of Quantified Cuts
What 


When 
May 06, 2013 from 02:00 PM to 03:00 PM 
Where  IF 2.33 
Add event to calendar 
vCal iCal 
Abstract:
We describe prooftheoretic results on cutelimination in classical firstorder logic and show how they lead to a method for abbreviating a cutfree proof by the introduction of lemmas.
The cutintroduction algorithm works by first computing a compressed representation of the terms present in the cutfree 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.