Temporal Description Logics: A Survey <s> Temporal Roles <s> I Introduction 1 Modal logic basics 1.1 Modal axiomatic systems 1.2 Possible world semantics 1.3 Classical first-order logic and the standard translation 1.4 Multimodal logics 1.5 Algebraic semantics 1.6 Decision, complexity and axiomatizability problems 2 Applied modal logic 2.1 Temporal logic 2.2 Interval temporal logic 2.3 Epistemic logic 2.4 Dynamic logic 2.5 Description logic 2.6 Spatial logic 2.7 Intuitionistic logic 2.8 'Model level' reductions between logics 3 Many-dimensional modal logics 3.1 Fusions 3.2 Spatio-temporal logics 3.3 Products 3.4 Temporal epistemic logics 3.5 Classical first-order logic as a propositional multimodal logic 3.6 First-order modal logics 3.7 First-order temporal logics 3.8 Description logics with modal operators 3.9 HS as a two-dimensional logic 3.10 Modal transition logics 3.11 Intuitionistic modal logics II Fusions and products 4 Fusions of modal logics 4.1 Preserving Kripke completeness and the finite model property 4.2 Algebraic preliminaries 4.3 Preserving decidability of global consequence 4.4 Preserving decidability 4.5 Preserving interpolation 4.6 On the computational complexity of fusions 5 Products of modal logics: introduction 5.1 Axiomatizing products 5.2 Proving decidability with quasimodels 5.3 The finite model property 5.4 Proving undecidability 5.5 Proving complexity with tilings 6 Decidable products 6.1 Warming up: Kn x Km 6.2 CPDL x K_m 6.3 Products of epistemic logics with Km 6.4 Products of temporal logics with Km 6.5 Products with S5 6.6 Products with multimodal S5 7 Undecidable products 7.1 Products of linear orders with infinite ascending chains 7.2 Products of linear orders with infinite descending chains 7.3 Products of Dedekind complete linear orders 7.4 Products of finite linear orders 7.5 More undecidable products 8 Higher-dimensional products 8.1 S5 x S5 x ... x S5 8.2 Products between K4 x K4 x ... x K4 and S5 x S5 x ... x S5 8.3 Products with the fmp 8.4 Between K x K x ... x K and S5 x S5 x ... x S5 8.5 Finitely axiomatizable and decidable products 9 Variations on products 9.1 Relativized products 9.2 Valuation restrictions 10 Intuitionistic modal logics 10.1 Intuitionistic modal logics with Box 10.2 Intuitionistic modal logics with Box and Diamond 10.3 The finite model property III First-order modal logics 11 Fragments of first-order temporal logics 11.1 Undecidable fragments 11.2 Monodic formulas, decidable fragments 11.3 Embedding into monadic second-order theories 11.4 Complexity of decidable fragments of QLogSU(N) 11.5 Satisfiability in models over (N,<) with finite domains 11.6 Satisfiability in models over (R,<) with finite domains 11.7 Axiomatizing monodic fragments 11.8 Monodicity and equality 12 Fragments of first-order dynamic and epistemic logics 12.1 Decision problems 12.2 Axiomatizing monodic fragments IV Applications to knowledge representation 13 Temporal epistemic logics 13.1 Synchronous systems 13.2 Agents who know the time and neither forget nor learn 14 Modal description logics 14.1 Concept satisfiability 14.2 General formula satisfiability 14.3 Restricted formula satisfiability 14.4 Satisfiability in models with finite domains 15 Tableaux for modal description logics 15.1 Tableaux for ALC 15.2 Tableaux for K(ALC) with constant domains 15.3 Adding expressive power to K(ALC) 16 Spatio-temporal logics 16.1 Modal formalisms for spatio-temporal reasoning 16.2 Embedding spatio-temporal logics in first-order temporal logic 16.3 Complexity of spatio-temporal logics 16.4 Models based on Euclidean spaces Epilogue. Bibliography. List of tables. List of languages and logics. Symbol index. Subject index. <s> BIB001 </s> Temporal Description Logics: A Survey <s> Temporal Roles <s> We combine the modal logic S5 with the description logic (DL) ALCQI. The resulting multi-dimensional DL S5ALCQI supports reasoning about change by allowing to express that concepts and roles change over time. It cannot, however, discriminate between changes in the past and in the future. Our main technical result is that satisfiability of S5ALCQI concepts with respect to general TBoxes (including GCIs) is decidable and 2-EXPTIME-complete. In contrast, reasoning in temporal DLs that are able to discriminate between past and future is inherently undecidable. We argue that our logic is sufficient for reasoning about temporal conceptual models with time-stamping constraints. <s> BIB002
Although already rigid roles are computationally difficult, there are cases where more expressive power is needed for talking about the temporal evolution of roles. In particular, it is natural to apply temporal operators not only to concepts, but also to roles. For example, to define roles 'will always be a member of' and 'will be a member of over and over again,' one can use the roles member of and ♦member of, respectively. Formally, a temporal role is a role name prefixed by a finite sequence of and ♦ operators, and the corresponding semantic clauses are Unfortunately, it is easy to modify the proof of Theorem 4 to show undecidability of concept satisfiability w.r.t. TBoxes in LTL ALC when TBoxes are allowed to contain a single temporal role of the form r: simply replace r by r in the reduction of the recurrent tiling problem. Without TBoxes, satisfiability of LTL ALC concepts with temporal roles has not yet been investigated. In fact, results have only been obtained for the case where LTL is replaced by standard modal logics such as K or S5  BIB001 BIB002 . We briefly discuss the S5 case. It has been argued in BIB002 that, for the encoding of temporal conceptual database models, it is often sufficient to use the operators ♦ u ('at some time point') and u ('at all time points') applied to concepts and roles, instead of LTL operators. The semantics of ♦ u is defined as and u is dual to ♦ u . Observe that ♦ u and u do not distinguish between future and past. For this reason, these operators behave exactly like the modal S5 operators, and we denote the resulting language by S5 ALC . The following result is proved in BIB002 . The technique used for proving the upper bound is an extension of a proof in  .