Efficient Proof Systems for Modal Logics

ESSLLI 2017 Course — 1st Week (17-21 July) — 14:00-15:30

Roman Kuznets & Lutz Straßburger


Modal logic has emerged as versatile, tractable language for reasoning about such disparate concepts as necessity, provability, obligation, time, space, knowledge, and belief. For reasoning to be efficient, one needs algorithms for deciding the problems of validity, satisfiability, etc. Many applications, including software and hardware verification, require constructing interpolants. One of the sources for these algorithms is structural proof theory, with its central, search-space limiting requirement of analyticity. While modern proof-theoretical methods can be traced back to Gentzen's work in the 1930s, for a long time modal logic has resisted systematic proof-theoretical study. Only recently has the advent of more powerful, more structural proof formalisms finally bucked the trend. This course will concentrate on sequent systems and their generalizations, starting from the introduction of basic concepts for the simplest case of sequent calculi and then discussing the constantly expanding range of modern proof-theoretic tools, including hypersequents and nested sequents.

In this course we will also teach many important proof theoretical concepts, including cut elimination, focusing, synthetic connectives, and interpolation, that are by no means restricted to the world of modal logics. We use modal logics only as a vehicle to explain these concepts in a uniform setting.

Tentative syllabus

Five 90-minute lectures are split into ten 45-minute units.


Main ESSLLI 2017 webpage

ESSLLI 2017 webpage for this course