zbMATH — the first resource for mathematics

Many-dimensional modal logics: theory and applications. (English) Zbl 1051.03001
Studies in Logic and the Foundations of Mathematics 148. Amsterdam: Elsevier (ISBN 0-444-50826-0/hbk). xviii, 747 p. (2003).
Many-dimensional modal logics result from combining different kinds of modal logical systems, each one of which involves a dimension that the other system(s) does (do) not involve, as, for instance, the logical systems yielded by mixing epistemic logic with temporal and/or spatial logic. This book is a research monograph on the construction of such modal logics, their properties with respect to their component logics (e.g., completeness, decidability and computational complexity) as well as directions of future investigations. The book mainly aims at researchers who use logic in computer science and artificial intelligence, but there are many parts of the book which would be of interest for pure logicians. The methods employed are basically semantical.
The book initially presents the motivation, syntax, semantics and applications of basic propositional modal logic. The semantic systems characterized are constituted by possible world semantic frames and models, though a brief description of algebraic semantics is also offered. Applications of basic modal logic include temporal logic, interval temporal logic, epistemic logic, dynamic logic, description logic, spatial logic and intuitionistic logic. The authors prove several theorems concerning the computational reductions (more precisely, polynomial reductions) between these different logics. We should note that first-order modal logic is not dealt with in this introductory part of the book but rather in later chapters, extensively and within the context of many-dimensional logics. In this connection, we should mention that the authors present a number of recent results concerning undecidable as well as decidable and axiomatizable fragments of first-order modal and temporal logics. And for several of these decidable fragments the authors determine their computational complexity.
Following the exposition of basic material, the authors consider two ways of constructing many-dimensional logic, namely: by fusions and by products. In fusions the operators of the combined modal systems do not interact at all, while in products their interactions are strong. The authors prove that completeness, the finite model property, decidability, decidability of the global consequence relation and interpolation are properties which will be transferred from the component logics to a fusion. They also show that the upper bounds for the computational complexity do not always transfer under the formation of fusions. The above positive general results for fusions cannot be obtained for products. This is shown by the authors by proving that certain products are not finitely axiomatizable, not decidable or not recursively enumerable, or lack the finite model property. But they also prove that other products are decidable or finitely axiomatizable when their component logis are. For these latter results, the authors introduce the method of quasimodels. Also, in the case of many of the decidable products, important theorems concerning their computational complexity are proved. The last four chapters of the book are dedicated mainly to applications of the techniques and results obtained in previous chapters to formalisms for knowledge representation. Here the authors analyze the computational behavior of temporal epistemic logics, description logics with modal and temporal operators and spatio-temporal logics. They also provide a decision procedure for modal description logics based on tableaux.

03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
03B45 Modal logic (including the logic of norms)
03B70 Logic in computer science
03B42 Logics of knowledge and belief (including belief change)
03B44 Temporal logic
03B20 Subsystems of classical logic (including intuitionistic logic)
03B25 Decidability of theories and sets of sentences
68T30 Knowledge representation