Proof Theory and Sequent Systems
Proof Theory and Sequent Systems
Lehrveranstaltung mit SWS 2/0/0 (Vorlesung/Übung/Praktikum) in SS 2024
Dozent
Umfang (SWS)
- 2/0/0
Module
Leistungskontrolle
- 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?
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, on the dates indicated in the schedule.
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.
