Lehrveranstaltungsleiter: A. Leitsch
First Meeting:
Monday October 10, 2:00 p.m.
Hörsaal 7,
Main Building, Karlsplatz 13
CONTENT:
Programming of Cut-elimination methods
In a project of the institute (supported by the Austrian Science Fund) efficient cut-elimination methods have been developed which turned out useful in transforming and analyzing mathematical proofs. The new method (CERES) is based on resolution and radically differs from traditional methods like those of Gentzen and Tait. For a deeper understanding of the new method an experimental comparison with Gentzen's and Tait's method can be quite helpful (in particular a comparison of the corresponding normal forms). The purpose of this project is to program the methods of Gentzen and Tait (and reductive methods in general), to perform experiments and to interpret the results. These experiments can be extended to the analysis of real mathematical proofs (which is the main topic of the research project).