Time:  12:00  13:20 
Room: 
Wean Hall 7201

Speaker: 
Stefan Hetzl Institute of Discrete Mathematics and Geometry Vienna University of Technology 
Title: 
Which proofs can be computed by cutelimination?

Abstract: 
In classical logic, it is typically possible to compute significantly different cutfree proofs from a single proof with cuts using a nondeterministic algorithm like Gentzen's procedure based on local proof rewriting steps. I will first speak about results that support this point by relating the number of cutfree proofs thus obtainable to the functions provably total in the system under consideration. Then I will turn towards recent work on characterising the cutfree proofs induced by a given proof with cuts. 