Proof Theory and Sequent Systems

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Proof Theory and Sequent Systems

Lehrveranstaltung mit SWS 2/0/0 (Vorlesung/Übung/Praktikum) in SS 2024


Umfang (SWS)

  • 2/0/0



  • Mündliche Prüfung

Course Description

Proof theory serves as one of the central pillars of mathematical logic and concerns the study and application of formal proofs. Typically, proofs are defined as syntactic objects inductively constructible through applications of inference rules to a given set of assumptions, axioms, or previously constructed proofs. Since proofs are built by means of inference rules, which manipulate formulae and symbols, proof theory is syntactic in nature, making proof systems well-suited for logical reasoning in a computational environment.

In this course, we will study fundamental concepts and techniques in proof theory, focusing in particular on sequent systems for propositional logic, first-order logic, and modal logic. We will discuss concepts such as admissible rules, invertible rules, cut elimination, and proof-search, as well as consider questions such as: How can we verify that a sequent system correctly captures a paradigm of logical reasoning? What techniques can be used to transform proofs into proofs of a desired shape? How can we mine proofs to extract additional information beyond the theorem being proved? How can we leverage a proof system for automated reasoning, which can be carried out by a computer?


Students are expected to be familiar with propositional logic. Familiarity with first-order logic or modal logic is helpful, but not necessary.

Course Plan

The course will take place on Fridays 9:20 – 10:50 in room APB E006. The first class will take place on 19 April 2024.


There will be an oral examination at the end of the course. To obtain a slot, please contact the instructor Dr. Tim Lyon by email.
  • The course script can be downloaded from the following website: [Link to Script]

Veranstaltungskalender abonnieren (icalendar)

Vorlesung Lecture 1 DS2, 19. April 2024 in APB E006
Vorlesung Lecture 2 DS2, 26. April 2024 in APB E006
Vorlesung Lecture 3 DS2, 3. Mai 2024 in APB E006
Vorlesung Lecture 4 DS2, 10. Mai 2024 in APB E006
Vorlesung Lecture 5 DS2, 17. Mai 2024 in APB E006
Vorlesung Lecture 6 DS2, 24. Mai 2024 in APB E006
Vorlesung Lecture 7 DS2, 31. Mai 2024 in APB E006