Modal logics, originally conceived in philosophy, have recently found many applications in computer science, artificial intelligence, the foundations of mathematics, linguistics and other disciplines. Celebrated for their good computational behaviour, modal logics are used as effective formalisms for talking about time, space, knowledge, beliefs, actions, obligations, provability, etc. However, the nice computational properties can drastically change if we combine some of these formalisms into a many-dimensional system, say, to reason about knowledge bases developing in time or moving objects. To study (...) the computational behaviour of many-dimensional modal logics is the main aim of this book. On the one hand, it is concerned with providing a solid mathematical foundation for this discipline, while on the other hand, it shows that many seemingly different applied many-dimensional systems (e.g., multi-agent systems, description logics with epistemic, temporal and dynamic operators, spatio-temporal logics, etc.) fit in perfectly with this theoretical framework, and so their computational behaviour can be analyzed using the developed machinery. We start with concrete examples of applied one- and many-dimensional modal logics such as temporal, epistemic, dynamic, description, spatial logics, and various combinations of these. Then we develop a mathematical theory for handling a spectrum of 'abstract' combinations of modal logics - fusions and products of modal logics, fragments of first-order modal and temporal logics - focusing on three major problems: decidability, axiomatizability, and computational complexity. Besides the standard methods of modal logic, the technical toolkit includes the method of quasimodels, mosaics, tilings, reductions to monadic second-order logic, algebraic logic techniques. Finally, we apply the developed machinery and obtained results to three case studies from the field of knowledge representation and reasoning: temporal epistemic logics for reasoning about multi-agent systems, modalized description logics for dynamic ontologies, and spatio-temporal logics. The genre of the book can be defined as a research monograph. It brings the reader to the front line of current research in the field by showing both recent achievements and directions of future investigations (in particular, multiple open problems). On the other hand, well-known results from modal and first-order logic are formulated without proofs and supplied with references to accessible sources. The intended audience of this book is logicians as well as those researchers who use logic in computer science and artificial intelligence. More specific application areas are, e.g., knowledge representation and reasoning, in particular, terminological, temporal and spatial reasoning, or reasoning about agents. And we also believe that researchers from certain other disciplines, say, temporal and spatial databases or geographical information systems, will benefit from this book as well. Key Features: Integrated approach to modern modal and temporal logics and their applications in artificial intelligence and computer science Written by internationally leading researchers in the field of pure and applied logic Combines mathematical theory of modal logic and applications in artificial intelligence and computer science Numerous open problems for further research Well illustrated with pictures and tables. (shrink)

The paper studies many-dimensional modal logics corresponding to products of Kripke frames. It proves results on axiomatisability, the finite model property and decidability for product logics, by applying a rather elaborated modal logic technique: p-morphisms, the finite depth method, normal forms, filtrations. Applications to first order predicate logics are considered too. The introduction and the conclusion contain a discussion of many related results and open problems in the area.

Dynamic topological logic provides a context for studying the confluence of the topological semantics for S4, topological dynamics, and temporal logic. The topological semantics for S4 is based on topological spaces rather than Kripke frames. In this semantics, □ is interpreted as topological interior. Thus S4 can be understood as the logic of topological spaces, and □ can be understood as a topological modality. Topological dynamics studies the asymptotic properties of continuous maps on topological spaces. Let a dynamic topological system (...) be a topological space X together with a continuous function f. f can be thought of in temporal terms, moving the points of the topological space from one moment to the next. Dynamic topological logics are the logics of dynamic topological systems, just as S4 is the logic of topological spaces. Dynamic topological logics are defined for a trimodal language with an S4-ish topological modality □ , and two temporal modalities, ○ and * , both interpreted using the continuous function f. In particular, ○ expresses f’s action on X from one moment to the next, and * expresses the asymptotic behaviour of f. (shrink)

Dynamic topological logic provides a context for studying the confluence of the topological semantics for S4, topological dynamics, and temporal logic. The topological semantics for S4 is based on topological spaces rather than Kripke frames. In this semantics, □ is interpreted as topological interior. Thus S4 can be understood as the logic of topological spaces, and □ can be understood as a topological modality. Topological dynamics studies the asymptotic properties of continuous maps on topological spaces. Let a dynamic topological system (...) be a topological space X together with a continuous function f. f can be thought of in temporal terms, moving the points of the topological space from one moment to the next. Dynamic topological logics are the logics of dynamic topological systems, just as S4 is the logic of topological spaces. Dynamic topological logics are defined for a trimodal language with an S4-ish topological modality □, and two temporal modalities, ○ and *, both interpreted using the continuous function f. In particular, ○ expresses f’s action on X from one moment to the next, and * expresses the asymptotic behaviour of f. (shrink)

We introduce the horizontal and vertical topologies on the product of topological spaces, and study their relationship with the standard product topology. We show that the modal logic of products of topological spaces with horizontal and vertical topologies is the fusion S4 ⊕ S4. We axiomatize the modal logic of products of spaces with horizontal, vertical, and standard product topologies.We prove that both of these logics are complete for the product of rational numbers ℚ × ℚ with the appropriate topologies.

We prove that S4 is complete with respect to Boolean combinations of countable unions of convex subsets of the real line, thus strengthening a 1944 result of McKinsey and Tarski 45 141). We also prove that the same result holds for the bimodal system S4+S5+C, which is a strengthening of a 1999 result of Shehtman 369).

The completeness of the modal logic S4 for all topological spaces as well as for the real line , the n-dimensional Euclidean space and the segment etc. was proved by McKinsey and Tarski in 1944. Several simplified proofs contain gaps. A new proof presented here combines the ideas published later by G. Mints and M. Aiello, J. van Benthem, G. Bezhanishvili with a further simplification. The proof strategy is to embed a finite rooted Kripke structure for S4 into a subspace (...) of the Cantor space which in turn encodes . This provides an open and continuous map from onto the topological space corresponding to . The completeness follows as S4 is complete with respect to the class of all finite rooted Kripke structures. (shrink)

Shehtman introduced bimodal logics of the products of Kripke frames, thereby introducing frame products of unimodal logics. Van Benthem, Bezhanishvili, ten Cate and Sarenac generalize this idea to the bimodal logics of the products of topological spaces, thereby introducing topological products of unimodal logics. In particular, they show that the topological product of S4 and S4 is S4 ⊕ S4, i.e., the fusion of S4 and S4: this logic is strictly weaker than the frame product S4 × S4. Indeed, van (...) Benthem et al show that S4 ⊕ S4 is the bimodal logic of the particular product space Q × Q, leaving open the question of whether S4 ⊕ S4 is also complete for the product space R × R. We answer this question in the negative. (shrink)