[ Lehrveranstaltungen 185/2 ]
[ AG Theoretische Informatik und Logik ]
[ Fachbereich Informatik ]
[ Technische Universität Wien ]

## Seminar in Theoretical Computer Science and Logic (185.300)

Lehrveranstaltungsleiter:
Alexander Leitsch

Diese Lehrveranstaltung ist Wahlfach im Magisterstudium *Computational Intelligence*.

**First Meeting:**

Monday, October 9 2006, 13:15

Zemanek-Hörsaal,

Favoritenstrasse 9, ground floor

**CONTENT:**

**Mathematical Applications of Cut-Elimination**

Cut-elimination is an important technique in proof theory. It serves the
purpose to eliminate lemmas from proofs and to produce normalized proofs
with the subformula property (the material of the whole proof can be obtained
by instantiations of subformulas of the theorem to be proved). In proof theory
cut-elimination is frequently used to prove consistency of logical systems.
Girard (in 1986) gave an interesting *mathematical* application of
cut-elimination: He demonstrated, that the Fürstenberg-Weiss
proof of van der Waerden's theorem on partitions (which is based on metric
spaces) can be transformed into van der Waerden's original elementary proof
via cut-elimination. This shows that cut-elimination can be used as a
technique to obtain elementary proofs from others wich apply higher-level
concepts. From these elementary proofs algorithms and effective constructions
can be extracted.

In this seminar, we discuss the cut-elimination theorem by G. Gentzen,
Girard's proof transformation on van der Waerden's theorem
(which was done by hand), and the recent development of
automated cut-elimination methods (CERES) for the transformation of
mathematical proofs.

A.Leitsch