Temporal Description Logics: A Survey <s> LTL ALC with Expanding Domains <s> We introduce a fundamental propositional logical system for describing correctness, termination and equivalence of programs. We define a formal syntax and semantics for the propositional modal logic of programs and give several consequences of the definition. Principal conclusions are that deciding satisfiability requires time d n/log n for some d > 1 and that satisfiability, even in an extended system, can be decided in nondeterministic time c n for some c. We provide applications of the decision procedure to regular expressions, Ianov schemes, and classical systems of modal logic. <s> BIB001 </s> Temporal Description Logics: A Survey <s> LTL ALC with Expanding Domains <s> Abstract We introduce a fundamental propositional logical system based on modal logic for describing correctness, termination and equivalence of programs. We define a formal syntax and semantics for the propositional dynamic logic of regular programs and give several consequences of the definition. Principal conclusions are that deciding satisfiability of length n formulas requires time d n /log n for some d > 1, and that satisfiability can be decided in nondeterministic time c n for some c . We provide applications of the decision procedure to regular expressions, Ianov schemes, and classical systems of modal logic. <s> BIB002 </s> Temporal Description Logics: A Survey <s> LTL ALC with Expanding Domains <s> In Baader (1990,1990a), we have considered different types of semantics for terminologicial cycles in the concept language TLQ which allows only conjunction of concepts and value-restrictions. It turned out that greatest fixed-point semantics (gfp-semantics) seems to be most appropriate for cycles in this language. In the present paper we shall show that the concept defining facilities of FLO with cyclic definitions and gfp-semantics can also be obtained in a different way. One may replace cycles by role definitions involving union, composition, and transitive closure of roles. ::: ::: This proposes a way of retaining, in an extended language, the pleasant features of gfp-semantics for FLQ with cyclic definitions without running into the troubles caused by cycles in larger languages. Starting with the language ALC of Schmidt-Schaus&Smolka (1988)--which allows negation, conjunction and disjunction of concepts as well as value-restrictions and exists-in-restrictions--we shall disallow cyclic concept definitions, but instead shall add the possibility of role definitions involving union, composition, and transitive closure of roles. In contrast to other terminological KR-systems which incorporate the transitive closure operator for roles, we shall be able to give a sound and complete algorithm for concept subsumption. <s> BIB003 </s> Temporal Description Logics: A Survey <s> LTL ALC with Expanding Domains <s> We show how to add full first-order temporal expressiveness to terminological logics. This can be achieved by embedding point-based tense operators in propositionally closed concept languages like ALC. The resulting temporal terminological logics are fully expressive over linear, Dedekind complete time such as ℕ and ℝ in the sense that all first-order temporal formulae over these time structures are expressible. We then prove that augmenting ALC by future-oriented tense operators interpreted over linear, discrete, unbounded time like IN does not increase its computational complexity. To establish this complexity result we show that coherence in ALC augmented by functional roles and their transitive closure is computable in polynomial space. We finally show how to obtain directly an axiomatization and a tableau-based algorithm for the tenselogical extension of terminological logics. <s> BIB004 </s> Temporal Description Logics: A Survey <s> LTL ALC with Expanding Domains <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> BIB005 </s> Temporal Description Logics: A Survey <s> LTL ALC with Expanding Domains <s> Fusions are a simple way of combining logics. For normal modal logics, fusions have been investigated in detail. In particular, it is known that, under certain conditions, decidability transfers from the component logics to their fusion. Though description logics are closely related to modal logics, they are not necessarily normal. In addition, ABox reasoning in description logics is not covered by the results from modal logics. In this paper, we extend the decidability transfer results from normal modal logics to a large class of description logics. To cover different description logics in a uniform way, we introduce abstract description systems, which can be seen as a common generalization of description and modal logics, and show the transfer results in this general setting. <s> BIB006
In this section and the subsequent one, we analyze the complexity of concept satisfiability in LTL ALC . We start by considering models with expanding domains because this case is particularly simple. Note first that constant domains and expanding domains give rise to different versions of concept satisfiability. For example, the following TBox has a (temporal) model with expanding domains, but no model with constant domains: A key observation regarding LTL ALC with expanding domains is that this logic is closely connected to the fusion of LTL and ALC, a general combination method for modal logics studied, e.g., in BIB006 BIB005 . To make this connection explicit, we introduce an alternative interpretation for LTL ALC . Let succ / ∈ N R be a special role name that is not allowed in LTL ALC concepts. A (non-temporal) interpretation I is called a fusion interpretation iff succ I is a total function. For d, e ∈ Δ I , we write d e to indicate that e is reachable from d by applying succ I to d zero or more times. To interpret an LTL ALC concept in I, we use the clauses from Section 2.1 together with the following ones: The following lemma due to Schild BIB004 shows that temporal interpretations with expanding domains and fusion interpretations are equivalent for LTL ALC concepts and TBoxes. be the root of the tree. We can rename the elements of Δ I so that for all r ∈ N R . It is now straightforward to convert I into a temporal interpretation I = I(0), I (1), . . . with expanding domains that is a model of C and T . For the 'only if' direction, it is straightforward to convert a temporal model I = I(0), I(1), . . . for C and T into a fusion interpretation shows that concept satisfiability in LTL ALC w.r.t. TBoxes and with expanding domains can be reduced to concept satisfiability w.r.t. TBoxes in any extension of ALC that provides for functional roles and allows us to express CUD under the fusion semantics given above (note that C can be expressed as ∀succ.C under this semantics). An example of such an extension is ALC with functional roles and the role operators known from propositional dynamic logic (PDL): composition, union, reflexive-transitive closure, and test BIB001 BIB003 . As shown in BIB004 BIB002 , satisfiability w.r.t. TBoxes is EXPTIME-complete in this DL, and PSPACE-complete if transitive closure can only be applied to functional roles and no TBoxes are admitted. These upper bounds thus transfer to LTL ALC with expanding domains, and corresponding lower bounds carry over from ALC.