LTG Logic and Theory Group

• Wednesday 16-18
• time and venue of exercises to be announced later

Lecture Room A97
Gebäude der Exakten Wissenschaften ("ExWi" building)
Sidlerstrasse 5

Proof theory is that subarea of mathematical logic which deals with formal proofs and formal provability. It has its origin in Hilbert’s program and was shaped by Gentzen’s seminal work in the nineteen-thirties. One of the central aims of proof theory is to understand the structure of formal proofs. To this end powerful deductive systems and proof methods have been developed which today also play an important role in computer science in connection with, for example, automated theorem proving, verification of programs and logic programming. In this course we consider in particular:

• Sequent calculi for classical and intuitionistic predicate logic
• Cut elimination and some consequences, the analysis of formal derivations, (automated) proof search
• Formulas as types, proofs as programs, and the Curry-Howard correspondence

This lecture is well suited for students who are interested in logic and in the foundations of mathematic and/or computer science. It provides an introduction into a research topic which has been actively pursued in the Bern group during the previous years.

Basic knowledge in mathematical logic and/or theoretical computer science.

To be announced during the lecture.