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 cut-elimination?
|
Abstract: |
In classical logic, it is typically possible to compute significantly different cut-free proofs from a single proof with cuts using a non-deterministic 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 cut-free proofs thus obtainable to the functions provably total in the system under consideration. Then I will turn towards recent work on characterising the cut-free proofs induced by a given proof with cuts. |