# Stefan Hetzl: Which proofs can be computed by cut-elimination?

Mathematical logic seminar – April 10, 2012
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.

### One response to “Stefan Hetzl: Which proofs can be computed by cut-elimination?”

1. More importantly, which proofs can be eliminated by cut-computation?