2024 Program

Week 1

To Be Announced

Week 2

To Be Announced

Interpolation through the Lens of Proof Theory
(Iris van der Giessen)

Keywords

Abstract

Craig interpolation is a fundamental concept in mathematical logic and computer science. Craig interpolants are formulas in a specified vocabulary that, intuitively speaking, explain why one formula entails the other. The existence of Craig interpolants is a useful property serving in many applications in database theory, knowledge representation, proof complexity, and more. For example, interpolants are used to enlarge knowledge bases by learning new concepts and the feasible extraction of interpolants from proofs relates to the NP vs co-NP problem. The goal of the course is to introduce theory and practice of interpolation through the lens of proof theory. Proof-theoretic techniques allow to explicitly construct interpolants which is useful in computations. We will discuss methods based on different systems such as sequent calculi and refutation systems. We will touch upon different version of Craig interpolation, such as Lyndon interpolation and uniform interpolation. We illustrate the applications of such methods in different fields including knowledge representation, formalized proofs, and proof complexity.

Pre-requisites

Lecturer