Proof Theory and Sequent Systems
Proof Theory and Sequent Systems
Course with SWS 2/0/0 (lecture/exercise/practical) in SS 2024
Lecturer
SWS
- 2/0/0
Modules
Examination method
- Oral exam
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?
Prerequisites
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.
Examination
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]
Subscribe to events of this course (icalendar)
| Lecture | Lecture 1 | DS2, April 19, 2024 in APB E006 | |
| Lecture | Lecture 2 | DS2, April 26, 2024 in APB E006 | |
| Lecture | Lecture 3 | DS2, May 3, 2024 in APB E006 | |
| Lecture | Lecture 4 | DS2, May 10, 2024 in APB E006 | |
| Lecture | Lecture 5 | DS2, May 17, 2024 in APB E006 | |
| Lecture | Lecture 6 | DS2, May 31, 2024 in APB E006 | |
| Lecture | Lecture 7 | DS2, June 7, 2024 in APB E006 | |
| Lecture | Lecture 8 | DS2, June 14, 2024 in APB E006 | |
| Lecture | Lecture 9 | DS2, June 21, 2024 in APB E006 | |
| Lecture | Lecture 10 | DS2, June 28, 2024 in APB E006 | |
| Lecture | Lecture 11 | DS2, July 5, 2024 in APB E006 |
Calendar
