Lehrveranstaltungsleiter: Alexander Leitsch
Diese Lehrveranstaltung ist Wahlfach im Magisterstudium Computational Intelligence (Bereich "Diskrete Mathematik und Logik").
Monday, March 7, 13:00
Favoritenstraße 9 / Stiege 1 / 3rd floor (yellow zone)
Methods of Cut-elimination
Cut-elimination introduced by Gerhard Gentzen in 1934 is the most prominent form of proof transformation in logic and plays an important role in automatizing the analysis of mathematical proofs. The removal of cuts corresponds to the elimination of intermediate statements (lemmas) from proofs resulting in a proof which is analytic in the sense, that all statements in the proof are subformulas of the result. Therefore, the proof of a combinatorial statement is converted into a purely combinatorial proof. Cut-elimination is therefore an essential tool for the analysis of proofs, especially to make implicit parameters explicit. In this course we first present the standard cut-elimination methods of Gentzen and Tait and give a mathematical comparison of the methods. In the second part we introduce CERES (cut-elimination by resolution) which is an efficient method essentially based on automated deduction. We show that CERES outperforms the methods of Gentzen and Tait and a larger class of methods based on stepwise proof reductions. Finally we give a presentation of CERES and illustrate the problems of cut-elimination in practice.