Handbook of Automated Reasoning

4.2 Modal logics

In this section, we cook the inverse method calculi for the propositional versions of several modal logics. As in the previous sections, we develop no semantics for these logics, instead we exploit proof-theoretic properties of cut-free sequent calculi for these logics. For standard formalizations and semantics of modal logics, see e.g. [Kripke 1963, Chagrov and Zakharyaschev 1996, Fitting and Mendelsohn 1998] and [Waaler 2001] (Chapter 22 of this Handbook). Proof-theoretic investigations of these logics can be found in [Fitting 1983]. The predicate versions of these logics are described in e.g. [Bowen 1979, Fitting 1983, Fitting and Mendelsohn 1998, Fitting, Thalmann and Voronkov 2000]. We discuss in some detail the design ...