Proof Theory and Sequent Systems

From International Center for Computational Logic

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