Kripke's worlds. An introduction to modal logics via tableaux (Q371440)

This book provides an \textit{accessible} introduction to modal logics indeed. In contrast to many standard textbooks it is focused on practical applicability of modal logics in reasoning tasks. In consequence, axiomatic treatment and metalogical matters like completeness proofs, interpolation etc. are avoided, but automatization and decidability are discussed in detail. There are three important features of this book worth mentioning: 1. Modal logics are treated in a very general way. Multimodal logics are introduced from the beginning and mainly via numerous examples followed by a more formal treatment. Except sketchy remarks on description logics one can find quite detailed treatment of automated reasoning in rather expressive logics like LTL (linear temporal logic) and PDL (propositional dynamic logic). One can find also a slightly less detailed presentation of hybrid logic. All logics are investigated from the semantical perspective with Kripke models treated as graphs. 2. The main interest of the authors lies in showing the applicability of modal logics in solving reasoning tasks like model checking, satisfiability checking, validity checking and model building. All of them are reduced to model building via tableaux. It should be noticed that the tableau method presented in this textbook differs in some respects from other known approaches. Two well-known tableau systems widely used in modal logic are Hintikka's approach, where sets of formulae are transformed by means of rules, and Fitting's approach, based on the use of labels denoting states (worlds) of Kripke models. In both approaches we are building one tree for a checked formula. In contrast to these approaches, the authors use tableaux with more graphs (premodels) involved, which makes it more similar to Kripke's original solution. However, in Kripke's system one builds a tree for every state of an attempted model, whereas in this approach one is building a graph for a Kripke model (nodes as states) and obtains more graphs in case of the application of branching rules. 3. The tableau method is presented via application of LoTREC (Logical Tableaux Research Engine Companion), which is a free software of generic character distributed by the Institut de Recherche en Informatique de Toulouse (IRIT) and accessible at {\texttt{http://www.irit.fr/Lotrec}}. Numerous examples and exercises allow the reader to smoothly develop her skills. In particular, several strategies of building graphs and obtaining termination are discussed. The book is well written and quite informative (despite neglecting some important issues which we mentioned above). It can be used as an easy-going introduction for all who are interested in automated reasoning and need some formal tools for playing with modal logics.