[ Lehrveranstaltungen 185/2 ]     [ AG Theoretische Informatik und Logik ]     [ Fakultšt Informatik ]     [ Technische Universitšt Wien ]

8.0 PR Project in Computational Logic

Lehrveranstaltungsleiter: A. Leitsch

First Meeting:

Monday October 10, 2:00 p.m.
Hörsaal 7,
Main Building, Karlsplatz 13


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).

Alexander Leitsch