# Efficient Proof Systems for Modal Logics

## Overview

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.
• Monday, July 17

• 01: Modal logic: syntax and semantics. Modal cube. (handout)
• Patrick Blackburn, Maarten de Rijke and Yde Venema: "Modal Logic". Cambridge University Press.
• A. S. Troelstra and H. Schwichtenberg: "Basic Proof Theory". Cambridge University Press.
• Edward John Lemmon and Dana S. Scott: "An Introduction to Modal Logic". Blackwell, Oxford, 1977.
• Jim Garson: "Modal logic". In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Stanford University, 2008.

• 02: Sequent systems. (handout)
• Gerhard Gentzen: "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift, 39:176-210, 1935. (online version)
• Gerhard Gentzen: "Untersuchungen über das logische Schließen. II". Mathematische Zeitschrift, 39:405-431, 1935.
• A. S. Troelstra and H. Schwichtenberg: "Basic Proof Theory". Cambridge University Press.

• Tuesday, July 18

• 03: Hypersequent systems. (handout)
• A. Avron: "The method of hypersequents in the proof theory of propositional non-classical logics". In W. Hodges, M. Hyland, C. Steinhorn, and J. Truss, editors, Logic: From Foundations to Applications. Clarendon Press New York, 1996 (Pdf)
• G. E. Minc: "Some calculi of modal logic", Logical and logical-mathematical calculus. Part I, Trudy Mat. Inst. Steklov., 98, 1968, 88-111; Proc. Steklov Inst. Math., 98 (1968), 97-124 (Pdf)
• Garrel Pottinger: "Uniform, cut-free formulations of T, S4, and S5", Journal of Symbolic Logic, 48(3): 900, 1983. (Pdf)
• Arnon Avron: "A Constructive Analysis of RM", Journal of Symbolic Logic, 52(4):939-951, 1987 (Pdf)
• Greg Restall: "Proofnets for S5: sequents and circuits for modal logic". In: "Logic Colloquium 2005", number 28 in Lecture Notes in Logic, pages 151-172. Cambridge University Press, 2007. (Pdf)
• Agata Ciabattoni, George Metcalfe, Franco Montagna: "Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions", Fuzzy Sets and Systems, 161(3): 369-389, 2010 (Pdf)
• Agata Ciabattoni, Nikolaos Galatos, Kazushige Terui: "From Axioms to Analytic Rules in Nonclassical Logics", LICS 2008, pages 229-240 (Pdf)
• Agata Ciabattoni, Lutz Straßburger, Kazushige Terui: "Expanding the realm of systematic proof theory", CSL 2009, (Pdf)
• Björn Lellmann: "Hypersequent Rules with Restricted Contexts for Propositional Modal Logics", Theoretical Computer Science, 656:76-105, 2016 (Pdf)
• Roman Kuznets and Björn Lellmann: "Grafting Hypersequents onto Nested Sequents", Logic Journal of the IGPL, 24(3):375-423, 2016 (Pdf)
• Hidenori Kurokawa: "Hypersequent Calculi for Modal Logics Extending S4", JSAI-isAI Workshops 2013, pp. 51-68 Springer 2014. (Pdf)
• Ori Lahav: "From Frame Properties to Hypersequent Rules in Modal Logics", LICS 2013, pages 408-417. (Pdf)

• 04: Nested sequent systems. (handout)
• K. Brünnler: "Deep sequent systems for modal logic". Arch. Math. Log., 48:551-577, 2009. (Pdf)
• Sonia Marin, Lutz Straßburger: "Label-free Modular Systems for Classical and Intuitionistic Modal Logics". AiML 2014 (Pdf)

• Wednesday, July 19

• 05: Decidability via proof formalisms. (handout)
• K. Brünnler: "Deep sequent systems for modal logic". Arch. Math. Log., 48:551-577, 2009. (Pdf)

• 06: Upper complexity bounds. (handout)
• Roman Kuznets and Björn Lellmann: "Grafting Hypersequents onto Nested Sequents", Logic Journal of the IGPL, 24(3):375-423, 2016 (Pdf)
• Michael Sipser "Introduction to the Theory of Computation", PWS Publishing Company, 1997
• J. Y. Halpern and L. C. Rêgo: "Characterizing the NP-PSPACE gap in the satisfiability problem for modal logic". Journal of Logic and Computation, 17, 795-806, 2007. (Pdf)
• R. E. Ladner: "The computational complexity of provability in systems of modal propositional logic", SIAM Journal on Computing, 6 (1977), pp. 467-480. (Pdf)
• Joseph Y. Halpern, Yoram Moses: "A guide to completeness and complexity for modal logics of knowledge and belief", Artificial Intelligence Volume 54, Issue 3, April 1992, Pages 319-379 (Pdf)

• Thursday, July 20

• 07: Focusing and synthetic connectives. (no handout)
• Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger: "Focused and Synthetic Nested Sequents". FoSSaCS 2016 (Pdf, extended version)
• Sonia Marin, Dale Miller, Marco Volpe: "A focused framework for emulating modal proof systems". AiML 2016. (Pdf)
• Dale Miller, Marco Volpe: "Focused labeled proof systems for modal logics". LPAR 20. LNCS 9450: 266-280. Springer, 2015. (Pdf)

• 08: Interpolation. (handout)
• W. Craig: "Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory". Journal of Symbolic Logic 22(3), 269-285 (1957) (Pdf)
• A. Troelstra, H. Schwichtenberg "Basic Proof Theory", Cambridge University Press, 2000.
• R. Kuznets: "Interpolation Method for Multicomponent Sequent Calculi". In "Logical Foundations of Computer Science, International Symposium, LFCS 2016, Deerfield Beach, FL, USA, January 4-7, 2016, Proceedings", LNCS v. 9537, pages 202-218. Springer, 2016. (Pdf)
• R. Kuznets: "Craig Interpolation via Hypersequents". In "Concepts of Proof in Mathematics, Philosophy, and Computer Science", "Ontos Mathematical Logic" v. 6, pages 193-214. De Gruyter, 2016. (Pdf)
• M. Fitting and R. Kuznets: "Modal Interpolation via Nested Sequents", Annals of Pure and Applied Logic, 166(3):274-305, 2015. (Pdf)
• R. Kuznets: "Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi". In "Logics in Artificial Intelligence, 15th European Conference, JELIA 2016, Larnaca, Cyprus, November 9-11, 2016, Proceedings", LNCS v. 10021 , pages 320-335. Springer 2016. (Pdf)

• Friday, July 21

• 09: Intuitionistic modal logics. (handout)
• A. S. Troelstra and H. Schwichtenberg: "Basic Proof Theory". Cambridge University Press.
• Alex Simpson: "The Proof Theory and Semantics of Intuitionistic Modal Logic". PhD Thesis, University of Edinburgh, 1994. (Pdf)

• 10: Intuitionistic nested sequent systems and focusing. (no handout)
• Lutz Straßburger: "Cut Elimination in Nested Sequents for Intuitionistic Modal Logics". FoSSaCS 2013 (Pdf)
• Sonia Marin, Lutz Straßburger: "Label-free Modular Systems for Classical and Intuitionistic Modal Logics". AiML 2014 (Pdf)
• Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger: "Modular Focused Proof Systems for Intuitionistic Modal Logics". FSCD 2016 (Pdf)