Temporal Description Logics: A Survey <s> Temporal DL-Lite <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 DL-Lite <s> We propose a new Description Logic, called DL-Lite, specifically tailored to capture basic ontology languages, while keeping low complexity of reasoning. Reasoning here means not only computing subsumption between concepts, and checking satisfiability of the whole knowledge base, but also answering complex queries (in particular, conjunctive queries) over the set of instances maintained in secondary storage. We show that in DL-Lite the usual DL reasoning tasks are polynomial in the size of the TBox, and query answering is polynomial in the size of the ABox (i.e., in data complexity). To the best of our knowledge, this is the first result of polynomial data complexity for query answering over DL knowledge bases. A notable feature of our logic is to allow for a separation between TBox and ABox reasoning during query evaluation: the part of the process requiring TBox reasoning is independent of the ABox, and the part of the process requiring access to the ABox can be carried out by an SQL engine, thus taking advantage of the query optimization strategies provided by current DBMSs. <s> BIB002 </s> Temporal Description Logics: A Survey <s> Temporal DL-Lite <s> We study the data complexity of answering conjunctive queries over Description Logic knowledge bases constituted by a TBox and an ABox. In particular, we are interested in characterizing the FOrewritability and the polynomial tractability boundaries of conjunctive query answering, depending on the expressive power of the DL used to express the knowledge base. What emerges from our complexity analysis is that the Description Logics of the DL-Lite family are essentially the maximal logics allowing for conjunctive query answering through standard database technology. <s> BIB003 </s> Temporal Description Logics: A Survey <s> Temporal DL-Lite <s> The use of ontologies in various application domains, such as Data Integration, the Semantic Web, or ontology-based data management, where ontologies provide the access to large amounts of data, is posing challenging requirements w.r.t. a trade-off between expressive power of a DL and efficiency of reasoning. The logics of the DL-Lite family were specifically designed to meet such requirements and optimized w.r.t. the data complexity of answering complex types of queries. In this paper we propose DL-Litebool, an extension of DL-Lite with full Booleans and number restrictions, and study the complexity of reasoning in DL-Litebool and its significant sub-logics. We obtain our results, together with useful insights into the properties of the studied logics, by a novel reduction to the one-variable fragment of first-order logic. We study the computational complexity of satisfiability and subsumption, and the data complexity of answering positive existential queries (which extend unions of conjunctive queries). Notably, we extend the LOGSPACE upper bound for the data complexity of answering unions of conjunctive queries in DL-Lite to positive queries and to the possibility of expressing also number restrictions, and hence local functionality in the TBox. <s> BIB004
In this section, we survey recent results on temporal DLLite. The DL-Lite family of lightweight DLs has been introduced and investigated in BIB002 BIB003 BIB004 with the aim of establishing maximal DLs for which the data complexity of query answering stays within LOGSPACE. In our brief survey, we consider three members of this family: the most expressive DL-Lite bool and its Horn and Krom fragments DL-Lite horn and DL-Lite krom . DL-Lite bool has the following concept constructors, for q ≥ 1: Concepts built only from the constructors marked with B are called basic. In contrast to ALC, DL-Lite bool has inverse roles (r − ) and number restrictions (≥ q r) which, however, are not qualified: a ∈ (≥ q r) I means that there are at least q distinct r-arrows starting from a, but the concept membership of their destination cannot be specified (thus ∃r.C is not expressible in DL-Lite bool ). DL-Lite horn is the sublanguage of DL-Lite bool with CIs of the form k B k B, for basic B, B k . Finally, DL-Lite krom allows only CIs of the form B 1 B 2 , B 1 ¬B 2 , ¬B 1 B 2 with basic B i . Note that all of these logics can say that a role r is functional: ≥ 2 r ⊥. Concept satisfiability w.r.t. TBoxes is NP-complete for DL-Lite bool , P-complete for DL-Lite horn , and NLOGSPACE-complete for DL-Lite krom ; see BIB004 and references therein. Consider now temporal extensions of these DLs. We survey what is currently known about the problem of deciding consistency of temporal LTL DL-Lite KBs with rigid roles, i.e., temporal operators can be applied to concepts, concept inclusions, and ABox assertions, and some roles may have a rigid interpretation. Note that only the application of Boolean operators to concepts (but not to CIs and ABox assertions) is restricted in temporal LTL DL-Lite krom KBs, and likewise for LTL DL-Lite horn . Recall that satisfiability of temporal LTL ALC TBoxes with rigid roles is highly undecidable by Theorem 4. As in the case of Theorem 10, it may thus look as if consistency of temporal LTL DL-Lite bool KBs with rigid roles is undecidable because we can easily enforce the existence of an × -grid. However, despite offering temporal operators on concepts, DL-Lite bool is not capable of expressing that adjacent tiles have the same colour. In fact, it turns out that temporal LTL DL-Lite bool TBoxes can be embedded into the one-variable fragment of first-order temporal logic, which is known to be EXPSPACE-complete; see, e.g., BIB001 . The converse embedding is also possible, and thus we obtain the following result. Theorem 11 ([6] ). Consistency of temporal LTL DL-Lite bool KBs with rigid roles is EXPSPACE-complete. The complexity of deciding consistency of temporal LTL DL-Lite krom KBs is an open problem. However, for temporal LTL DL-Lite krom KBs in which only the next-time operator is applied to basic concepts within CIs, consistency is PSPACE-complete. The proof of this result uses the fact that there are polynomially many CIs that are consequences of a set of Krom CIs (they are Krom CIs as well), and the 'local' character of the operator applied to concepts. In contrast, for temporal LTL DL-Lite horn KBs, the following rather surprising result can be shown by encoding the EXPSPACEcomplete × 2 n corridor tiling problem.