A knowledge base is a finite set of terminological and assertional axioms. An interpretation I is a model of a knowledge base i every axiom of is satisfied by I. logically for every model of implies written we say that if is subsumed by    in   . The reasoning problem of checking whether    is subsumed by in is called subsumption checking.    logically implies written for every model of     we say that    is an instance of    in   . The reasoning problem of checking whether is an instance of in is called instance recognition.

An acyclic simple T  ox can be transformed into an  expanded T  ox having the same models, where no defined concept makes use in its definition of any other defined concept. In this way, the interpretation of a defined concept in an expanded T  ox does not depend on any other defined concept.  It is easy to see that     is subsumed by     in an acyclic simple Tox if and only if the expansion of with respect to wis subsumed by the expansion of with respect to in the empty T  ox. The expansion procedure recursively substitutes every defined concept occurring in a definition with its defining expression  such a procedure to may generate a T  ox exponential in size, but it has been proved  Nebel, that it works in polynomial time under reasonable restrictions. The following interchangeably refers either to reasoning with respect to a T  ox or to reasoning involving expanded concepts with an empty T ox. In particular, while devising the subsumption calculus for the logics considered here, it is always assumed that all defined concepts have been expanded.

## 3. Towards A Temporal Description Logics

proposed to extend   escription   ogics with an interval based temporal chmiedel logic. The temporal variant of the escription ogic is e uipped with a model-theoretic ss onini et al.,
it di ers from ALCF in that it does not contain the and concepts, it does not have neither negation nor dis unction, and it has cardinality restrictions and con unction over roles. The new temporal term-forming operators are the temporal ualifier at, the existential and universal temporal uantifiers sometime and alltime. The ualifier operator specifies the time at which a concept holds. The temporal uantifiers introduce the temporal variables constrained by means of temporal relationships based on Allen s interval algebra extended with metric constraints to deal with durations, absolute times, and granularities of intervals. To give an example of this temporal escription ogic, the concept of Mortal can be defined by

## Mortal Livingbeing Π (Sometime X After X Now   At X   Livingbeing  )

with the meaning of a LivingBeing at the reference interval NOW, who will not be alive at an interval x sometime after the reference interval NOW.  chmiedel does not propose any algorithm for computing subsumption, but gives some preliminary hints. Actually, cc
, sacrificing the main benefit escription ogics the possibility of having decidable inference techni ues.

of chmiedel s temporal   escription   ogic, when closed under complementation, contains as a proper fragment the temporal logic     proposed by  alpern and  hoham is a propositional modal logic which extends propositional logic with modal The logic formul   of the kind      .   and     .

where is a basic Allen s temporal relation and