Temporal Description Logics: A Survey <s> Rigid Roles <s> Massachusetts Institute of Technology. Dept. of Electrical Engineering. Thesis. 1974. Ph.D. <s> BIB001 </s> Temporal Description Logics: A Survey <s> Rigid Roles <s> Elementary translations between various kinds of recursive trees are presented. It is shown that trees of either finite or countably infinite branching can be effectively put into one-one correspondence with infinitely branching trees in such a way that the infinite paths of the latter correspond to the “ P -abiding” infinite paths of the former. Here P can be any member of a very wide class of properties of infinite paths. For many properties ??, the converse holds too. Two of the applications involve (a) the formulation of large classes of highly undecidable variants of classical computational problems, and in particular, easily describable domino problems that are III 1 1 -complete, and (b) the existence of a general method for proving termination of nondeterministic or concurrent programs under any reasonable notion of fairness. <s> BIB002 </s> Temporal Description Logics: A Survey <s> Rigid Roles <s> This chapter considers, on the one hand, extensions of Description Logics by features not available in the basic framework, but considered important for using Description Logics as a modeling language. In particular, it addresses the extensions concerning: concrete domain constraints; modal, epistemic, and temporal operators; probabilities and fuzzy logic; and defaults.On the other hand, it considers non-standard inference problems for Description Logics, i.e., inference problems that - unlike subsumption or instance checking - are not available in all systems, but have turned out to be useful in applications. In particular, it addresses the non-standard inference problems: least common subsumer and most specific concept; unification and matching of concepts; and rewriting. <s> BIB003 </s> Temporal Description Logics: A Survey <s> Rigid 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> BIB004
In DL, additional constraints for roles have become an important means to increase the expressive power. A typical example is the introduction of transitive roles or role inclusions. In TDL, the most important constraint of this type is rigid roles. A role r has a rigid interpretation in I if The role geographical part of is a typical rigid role, whereas member of will mostly be non-rigid. We remark that, in contrast to roles, no additional constraints are required to express that a concept is rigid: the CIs C C and ¬C ¬C imply that This result can be proved by reduction of a well-known Σ 1 1 -complete problem, namely the recurrent tiling problem BIB002 : given a set S = {t 0 , . . . , t n } of tile types, decide whether it is possible to cover the × -grid with tiles of these types such that t 0 appears infinitely often in the first row. Recall that each t i is a 4-tuple of colours , and a tile of type t j can be a right (up) neighbour of a t i -tile only if right( . We encode this problem in LTL ALC with a single rigid role r. Let A 0 , . . . , A n be concept names representing the given tile types, and let the TBox T contain the following CIs: Then the concept ♦A 0 is satisfiable w.r.t. T iff S can tile the × -grid with tiles of type t 0 appearing infinitely often in the first row. We sketch the proof of the 'only if' direction. Let (0, d 0 ) be an instance of ♦A 0 in a model I of T . By the first CI in T , there is an infinite sequence . . at time point 0. We can use it as the first column of the grid. Since r is a rigid role, this sequence is found also at any other time point, which gives us the rest of the grid. By the second and third CIs, every point of the grid is covered by a unique tile, and the last two CIs guarantee that the colours of the tiles match. In the reduction above, one dimension of the grid is implicit in the flow of time. The second dimension is generated by the infinite chain enforced by the first CI in T . Without TBoxes or with only acyclic ones (see BIB003 for a definition), such a chain cannot be enforced. In these cases, concept satisfiability becomes decidable, though it is still very expensive. The intuition behind the proof of this result is as follows. Define the role depth rd(C) of an LTL ALC concepts C as the number of nestings of existential restrictions ∃r in C. For example, rd(A ∃r.B) = 1 and rd(∃r 1 .(B ∃r 2 .A)) = 2. In the same way as for ALC, one can show that any satisfiable LTL ALC concept C is satisfiable in a temporal interpretation I in which no path (n, d 0 )r I (n, d 1 )r I · · · r I (n, d k ) has length larger than rd(C). Thus, it is not possible to generate the infinite second dimension of an × -grid. However, the complexity of deciding satisfiability of a concept C still grows superexponentially with rd(C), and in BIB004 it is shown that the satisfiability problem for concepts C with rd(C) ≤ n is nEXPSPACE-complete, for all n ≥ 1. The lower bound is proved using the yardstick technique of Stockmeyer BIB001 and the upper bound uses, in addition to the bound on the length of paths, the fact that each I(n) can be assumed to be tree-shaped. We will return to the issue of rigid roles in Section 5.