A formalization of interval-based temporal subsumption in first order logic

We are investigating interval-based temporal extensions of terminological logics. These extensions allow to model temporally rich domains with a terminological approach. The first part of the paper presents the extension of known terminological logics by adding temporal operators on intervals and providing a new semantics. Reasoning on taxonomies of time-dependent concepts defined with these logics involves computing a subsumption relation. We briefly describe what is known about un/decidability of subsumption and incomplete algorithms, but the emphasis of this paper is on a translation from these logics into a first order logic with two sorts. The temporal subsumption problem is reduced to validity for a subset of formulae. This translation formalizes the known relation between terminological and predicate logics, extending it to interval-based temporal operators. Through the translation we show that subsumptions are recursively enumerable for a class of these logics having as temporal domain the set of intervals defined as ordered pairs of rational numbers. We also show how ordinary theorem provers can be used as semi-automatic tools to prove temporal subsumption