Efficient Proof Systems for Modal Logics

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.