Temporal Description Logics: A Survey <s> Introducing LTL ALC <s> 1. The handling of time: introduction and survey 2. Semantical presentation of temporal connectives 3. Axiomatic presentation of propositional temporal connectives 4. Predicate temporal logics 5. Temporal logics presented in the predicate calculus: language-metalanguage 6. A general theory of axiomatization for propositional temporal logic 7. Basic many-dimensional systems 8. Propositional quantifiers and fixed point operators 9. Expressive power of one-dimensional temporal connectives: basic concepts 10. Expressive completeness of Since and Until over integer and real time 11. Expressive completeness of Stavi connectives over general linear time 12. Further expressive completeness results 13. H-dimension 14. Adding a temporal dimension to a logic system 15. Decidability in temporal logic Bibliography Notation Index Index of Systems Index <s> BIB001 </s> Temporal Description Logics: A Survey <s> Introducing LTL ALC <s> This paper introduces a new logical formalism, intended for temporal conceptual modelling, as a natural combination of the well-known description logic DLR and point-based linear temporal logic with Since and Until. We define a query language (where queries are non-recursive Datalog programs and atoms are complex DLRUS expressions) and investigate the problem of checking query containment under the constraints defined by DLRUS conceptual schemas--i.e., DLRUS knowledge bases--as well as the problems of schema satisfiability and logical implication. <s> BIB002 </s> Temporal Description Logics: A Survey <s> Introducing LTL ALC <s> In this paper we introduce a decidable fixpoint extension of temporal Description Logics. We exploit the decidability results obtained for various monodic extensions of Description Logics to obtain decidability and tight complexity results for temporal fixpoint extensions of these Description Logics and more generally for the decidable monodic fragments of first order logic. <s> BIB003 </s> Temporal Description Logics: A Survey <s> Introducing LTL ALC <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
We define the temporal description logic LTL ALC whose concepts are formed using the concept constructors of ALC enriched with the temporal constructors C and CUD, as known from propositional linear time temporal logic (LTL); see, e.g., BIB001 . As usual, we use ♦C as an abbreviation for UC and C for ¬♦¬C. TBoxes are defined in the same way as in the case of ALC, but now using LTL ALC concepts instead of ALC concepts. For simplicity, we work without ABoxes for now. For example, the following CI states that any non-EU country has to be first an EU member candidate before it can be become an EU member: ¬EU member ♦EU member ♦(EU candidate U EU member). Like in propositional LTL, we can further enrich LTL ALC by adding additional temporal operators, e.g., past operators for 'at the previous moment' and 'since'  BIB002 or fixedpoint operators BIB003 . For the purposes of this paper, we will concentrate on and U, and only mention additional temporal operators when necessary. The semantics of LTL ALC is based on temporal interpretations. To extend · I to composite concepts, we use the same clauses as in Section 2.1 for the Booleans, plus the following ones: Thus, the CIs of a TBox are regarded as temporally global constraints in the sense that they should hold at every moment of time. An LTL ALC concept C is satisfiable w.r.t. a TBox T if there is a common model of C and T . It is not hard to see that this is equivalent to saying that there is a model I of T with C I = ∅. The problem of concept satisfiability w.r.t. TBoxes in LTL ALC is to decide, given a concept C and a TBox T , whether C is satisfiable w.r.t. T . Intuitively, LTL ALC can be viewed as a two-dimensional combination of ALC with LTL BIB004 . If we treat concept names as propositional variables of LTL, then every temporal interpretation I and every element d ∈ Δ I give rise to the LTL structure M d defined by In this sense, the roles in LTL ALC are a second dimension: they allows us to switch between different LTL structures  In spite of this effect, the interaction between LTL and ALC in LTL ALC is actually rather weak, as illustrated in the next section.