# FG1 Seminar talk

2014-10-31

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

Abstract:

This talk will be about the sequent calculus and cut-elimination in classical
first-order logic.

Gentzen's proof of the cut-elimination theorem can be considered as a non-deterministic procedure based on local proof rewriting steps. I will speak about some recent results concerned with describing the set of cut-free proofs thus obtainable from a fixed proof with cuts.

I will not assume any prior knowledge in proof theory.