We design and investigate a new interval based temporal description logic, EL , which is based on an Annotated Logic introduced by Kifer, AL, and motivated by life-science applications. We show how a subset of the logic can be captured as the EL fragment of AL, ELAL, and then go on to show how we can extend this representation to capture further temporal entailments. We show that both ELAL and EL maintain the same tractable complexity bounds for reasoning as EL and finally provide an example of how the logic can be utilised for the Drosophila developmental ontology.
Introduction
“ C located_in C’ if and only if: given any c that instantiates C at a time
t, there is some c’ such that: c’ instantiates C’ at time t and c located_in
c’ ”. [22]
It is clear that temporal information is needed and wanted, but can not be
captured due to limitations of current DLs. Temporal information is also present
in many developmental ontologies in the bio-medical domain. These ontologies
often express their time content in terms of stages (often referred to as Theiler
stages) which are usually represented in a linear discrete time sequence. The
temporal information of theses stages is usually stored as OWL annotations
on classes and not included in the formal definition of the ontology. An example
focussing on developmental stages is the Drosophila ontology [
It seems that the expressive powers of current TDLs are somewhat of an overkill for these applications that mention specific moments in time and stages. For example, the operator (some future moment) expresses time information where specific time points are not known (uncertainty). They also consider time to be relative and over an infinite sequence of time points, whereas the applications need more of an absolute time representation where we only need a few time points of a finite sequence.
In this paper we investigate and design two TDLs based on an interval
representation of time using exact time points, with the aim to provide a suitable
TDL for developmental ontologies. Our first attempt is based on an Annotated
Logic (AL) introduced by Kifer [
Preliminaries
ELH & EL We assume the reader to be familiar with the syntax and semantics
of ELH and EL [
First Order Logic We assume the reader to be familiar with first order logic, and will use the standard notion of a valuation, i.e., a mapping from free variables into interpretation domain elements and, for x a variable name, the x-variant of a valuation , i.e., the valuation 0 that behaves exactly like but for possibly mapping x to a different domain element.
Annotated Logics (ALs) are formalisms that have been applied to knowledge
representations and expert systems, first introduced in [23] and later studied
in [
We use ID(SL) for the set of all ideals of SL. Furthermore, we assume that the lattice comes with a unary (pseudo) complement operator :.
A generalized interpretation I = ( I ; I( ); SL) consists of a non-empty domain I and a mapping I( ) that maps (i) each constant symbol a to an element I(a) 2 I and (ii) each n-ary predicate symbol P and each tuple a1; : : : ; an ( I )n to an ideal S 2 ID(SL). The interpretation is extended to formulae as follows: let I be a generalized interpretation, a valuation, 2 SL, A a ground atom, and F a formula. Then: 1. I; j= A(t1; : : : ; tn) : if 2 I(A(e1; : : : ; en)), where ei = I(ti) if ti is a constant and ei = (ti) if ti is a variable,
As usual, I is said to be a model of a formula F if I j= F . To illustrate the semantics of AL when combined with a DL, let us first extend the semilattice to handle time intervals: Definition 2. An interval is of the form [x; y] where x; y 2 N and x y. For an interval = [x; y], x is the start point of and is denoted as s and similarly y is the end point of and shall be denoted as e. Let (SL; ) be a semi-lattice of intervals upwards closed by an interval denoted as >. Let 1; 2 2 SL. The ord2erSiLngs.t 6 i9s a0s2foSllLowasn:d 1 0s<< 2 siff. Les1t maxs2(aSnLd) =e1 e fe2o.r Let2mSiLn(sS.Lt)69=0 2s fSoLr and 0e > e. > = [SLmin; SLmax].
In this paper we focus on representing time as a discrete linear sequence,
similar to the representation of time in LTL where we have exactly one future
moment in time (discrete) and only one time sequence (linear). We do not state
any assumption on the time between points x and x + 1. Consider the following
AL formulae annotated with intervals (the semilattice for the annotations of the
formulae is depicted in Figure 2):
1. 8x B[1;1](x) ) A[1;2](x)
2. 8x 9y A[1;1](x) ) R[1;3](x; y) ^ C[1;2](y)
3. 8x 9y R[1;1](x; y) ^ C[1;1](y) ) D[2;3](x)
4. A[1;3](d)
We interpret the formulae above as follows: (1) All instances of B at time 1 are
instances of A at times 1 and 2, (2) All instances of A at time 1 have some
R-relation at times 1, 2 and 3 to an individual who is an instance of C at times 1
and 2, (3) All instances who have an R successor at time 1 to some instance who
is a C at time 1, are instances of D at times 2 and 3, (4) d is an instance of A
at times 1, 2 and 3. To show how the lattice interacts with formulae and ideals,
consider the following example. Using the lattice from Figure 2, and a formula
A[1;3](d), the ideal of ID([1; 3]) is {[
We now combine the semantics of AL and EL to form ELAL- our first attempt at temporalising EL with time intervals based on AL. ELAL concept descriptions extend EL concept descriptions with the use of intervals (which we may refer to as labels) occurring in a semilattice SL and appearing on atomic concepts and roles. Concept descriptions in ELAL are defined according to the following definition: Definition 3. Let SL be a semilattice of intervals, 2 SL an arbitrary interval, A an atomic concept, R an atomic role (role name) and C, D arbitrary concept descriptions. Then concept descriptions are formed in ELAL according to the following syntax rule:
C; D
! > > j A j C u D j 9R :C
Definition 4. An interpretation I = h I ; I i, consists of a non empty set I which is the domain of I, and a function I that maps individuals to elements of I , each concept name A I and each role name R I I . The function I is inductively extended to arbitrary concepts by setting – >I = I – (C u D)I = CI \ DI – (9R 1 :C)I = fx 2
I j 9y 2 CI ^ (x; y) 2 RI1 g as well as the following restrictions on the domain reflecting the general semantics from AL:
An ELAL knowledge base (KB) is made up of three parts: a terminological
part called the TBox, denoted as T , an assertional part called the ABox, denoted
as A and a semilattice of time intervals SL. The TBox and ABox are defined as
usual. It is clear that the added restrictions on interpretations I of ELAL capture
the semantics of AL because, the only additional implications we have are that
when 1 2, 8x : A 2 (x) ! A 2 (x). We aim to show that subsumption in
ELAL can be decided in polynomial time, and we do this by utilising an existing
decision procedure for ELH. We give a polynomial time reduction to show that
any ELAL KB can be converted into a classical ELH KB s.t. they are model
preserving. Our reduction consists of unfolding the restrictions (1 & 2) into the
KB, enabling us to remove the lattice and have an equisatisfiable ELH KB.
Reduction We unfold the restrictions on the domain of ELAL into an ELH KB,
similar to the reduction found in [
n T 0 :=T [
A 1 v A 2 j A 1 ; A 2 2 Te ^ R :=
R 1 v R 2 j R 1 ; R 2 2 Te ^ Since R(K) involves no semilattice, we treat labelled concept names as usual ELH concept names. It is clear that for any model I of K, I is also a model of R(K), as the only axioms added to K are those already satisfied in I. It is also clear that for any model I of R(K), I is also a model of K since the added axioms in R(K) ensure that the additional constraints of I have been met. Lemma 1. Let K=(T ,A,SL) be an ELAL KB. K and R(K) have the same models.
The maximum number of additional axioms in R(K) is limited quadratically w.r.t |K|. The reduction can be computed deterministically and since there are only a quadratic number of additional axioms that can be added, the reduction only requires polynomial time.
Lemma 2. Let K= (T ,A,SL) be an ELAL KB. R(K) can be computed in polynomial time w.r.t jKe j.
Finally, as we are now left with an ELH KB, we can utilise the reasoning
procedures from ELH to compute subsumption. It was shown in [
Corollary 1. Computing subsumption in ELAL is PTime-Complete. Limitations of ELAL According to the semantics of the semilattice from AL, the lattice really is just a set of labels, and even if we consider those labels to be intervals, the only temporal information they carry is that an interval is contained within another. Crucially, they do not capture an important aspect of temporal information involving overlapping intervals. Consider a semilattice of intervals with elements f[1; 4]; [2; 5]; [3; 6]; [1; 7]g, and a TBox T := fC[1;7] v A[1;4] u A[3;6]; A[2;5] v D[1;7]g. Since the interval [2; 5] is not contained within the intervals [1; 4] or [3; 6], there is nothing to tell us that the interval is contained within the conjunction of the two, i.e we want T to entail that C[1;7] v D[1;7]. It is not obvious how to recode the lattice to capture this. We could fix the issue by extending the domain constraints, however it is clear that the semantics of AL is not enough to capture minimal temporal information using our current ordering. Other issues arise when we consider the possibility of varying domains and possible worlds. In AL we are restricted to a single “world” with a constant domain, but TDLs can adopt a possible world semantics allowing the possibility of varying domains. It is not clear how to extend ELAL to capture this. To overcome these 2 problems, we move towards a new version of an interval based EL with a possible worlds semantics. 4
We now consider temporalising EL with time intervals by adopting a possible worlds semantics [24]. We use the same definition for intervals as in Section 3. EL concept descriptions are built in the same way as ELAL concept descriptions, however the intervals need no longer appear in a semilattice. In EL , the semantics of concept descriptions is defined in terms of a temporal interpretation with possible worlds. The possible worlds are a finite sequence of normal EL interpretations indexed by i 2 N.
Definition 6. An EL interpretation I = ( I ; Ii ; I ) consists of a non-empty (constant) domain I and a function Ii that, for each index i 2 fm; :::; ng N, maps each concept name A to a subset AIi I , each role name R to a subset RIi I I , where i is an index for each possible world. The function Ii is inductively extended to arbitrary concepts by setting – >Ii = I – (C u D)Ii := CIi \ DIi – (9R:C)Ii := fe 2 I j 9f 2 CIi ^ (e; f ) 2 RIi g I is a global function which maps each labelled concept name A[x;y] to A[Ix;y] = Tx i y AIi , and each role R[x;y] to R[Ix;y] = Tx i y RIi . The function I is inductively extended to arbitrary concepts with labelled elements as follows: – >I = I – (C u D)I := CI \ DI – (9R :C)I := fe 2 I j 9f 2 CI ^ (e; f ) 2 RI g Since we now have two types of concepts: A and A (similarly with role names), we differentiate between the two by declaring Ncon as the unlabelled counter parts of concepts occurring in Ncon (similarly with Nrole and Nrole). A[Im;n] if x < u Lemma 3. For any I, (1) A[Ix;y] y + 1 v, m
A[Iu;v] if x u v y. (2) A[Ix;y] \ A[Iu;v] x, n v. (Similarly, for each role name R ).
Lemma 3.1 establishes that we capture the same constraints on the domain as ELAL, whilst Lemma 3.2 overcomes the known limitations of ELAL by capturing the overlapping intervals correctly.
An EL KB is built in the same way as an ELAL KB without the need of a semilattice. 4.2
As usual, we rely on an EL subsumption.
Definition 7. Let T be an EL -TBox over the set Ncon and Nrole. T is normalised iff T contains only GCIs of the forms: where A i ; B i ; C i are atomic concept names from Ncon and R i is a role name from Nrole.
This normal form is similar to those seen in [
– INIT0 S0(A ) := f>; A g for every A 2 Ncon , – INIT1 S0(R ) := fR g for every R 2 Nrole – CR0 If A[x;y] 2 Si(C 1 ) and D 2 2 Si(A[u;v]) where x u v y and
D 2 62 Si(C 1 ) then Si+1(C 1 ) := Si(C 1 ) [ fD 2 g – CR1 If A 1 v B 2 2 T and A 1 2 Si(C 3 ) and B 2 2= Si(C 3 ) then
Si+1(C 3 ) := Si(C 3 ) [ fB 2 g. – CR2 If A 1 u B 2 v C 3 2 T and A 1 ; B 2 2 Si(D 4 ) and C 3 2= Si(D 4 ) then Si+1(D 4 ) := Si(D 4 ) [ fC 3 g. – CR3 If A 1 2 Si(B 2 ) and A 1 v 9R 3 :C 4 2 T and D 5 2 Si(C 4 ) and P 6 2 Si(R 3 ) and 9P 6 :D 5 v E 7 2 T and E 7 62 Si(B 2 ) then Si+1(B 2 ) := Si(B 2 ) [ fE 7 g. – CR4 If B 1 2 Si(C[x;y]) and C[i;j] 2 Si(A 2 ) and C[k;l] 2 Si(A 2 ) and i < k j + 1 l and x i and y l and B 1 62 Si(A 2 ) then Si+1(A 2 ) := Si(A 2 ) [ fB 1 g – CR5 If R[x;y]; R[u;v] 2 NrTole and x u v y and R[u;v] 62 Si(R[x;y]) then
Si+1(R[x;y]) := Si(R[x;y]) [ fR[u;v]g
Theorem 1. Let T be an EL -TBox over the set Ncon and Nrole. For every
F 1 ; G 2 2 Ncon (or Nrole), it holds that G 2 2 S (F 1 ) iff T j= F 1 v G 2 .
Proof We first show the ) direction by proof of induction over n. Due to space
constraints, we only include a proof for the most interesting rules. The full proof
can be found in [
Claim: G 2 2 S (F 1 ) ) T j= F 1 v G 2 n = 0: If INIT0 added G 2 to Sn(F 1 ), then G 2 =F 1 or G 2 =>, proving the claim holds. n > 0: If CR4 added G 2 to Sn(F 1 ) then there exists a concept C[x;y] where G 2 2 Sn 1(C[x;y]) and C[i;j] 2 Sn 1(F 1 ) and C[k;l] 2 Sn 1(F 1 ) and i < k j + 1 l and x i and y l and G[u;v] 62 Sn 1(F 1 ). By induction hypothesis it holds that T j= C[x;y] v G 2 , T j= F 1 v C[i;j] and T j= F 1 v C[k;l]. From Lemma 1 and Lemma 2, T j= F 1 v C[x;y], therefore by transitivity of subsumption it holds that T j= F 1 v G 2 proving the claim.
It suffices to show T j= F 1 v G 2 ) G 2 2 S (F 1 ). We approach this by
proving the contraposition: Claim: G 2 2= S (F 1 ) ) T 6j= F 1 v G 2 where we
build a canonical model I of T with a witness x 2 F I1 n GI2 . We construct the
canonical model I according to the following definition:
– CM0 I = fa 1 j A 1 2 Ncong
– CM1 AIi = fb 1 j x i y and A[x;y] 2 S (B 1 )g
– CM2 RIi = f(a 3 ; b 4 ) j x i y and C 1 v 9P 2 :B 4 and C 1 2 S (A 3 )
and R[x;y] 2 S (P 2 )g
We first show that I is in fact a valid model of T . Since T is normalised, it
suffices to show that the model is valid for each of the four possible axioms in T .
Again, due to space constraints, we only include a proof for the most interesting
axioms. The full proof can be found in [
– A 1 v B 2 2 T ! AI1 BI2 . Let y 3 2 AI1 . By definition of CM1 A 1 2 S (Y 3 ). By non-applicability of CR1 B 2 2 S (Y 3 ), thus by definition of CM1 y 3 2 BI2 .
As we have shown that I is a model of T , it remains to show that F I1 6 GI2 when
G 2 62 S (F 1 ) by finding a witness y 3 2 F I1 n GI2 . Claim: G 2 62 S (F 1 ) )
F I1 6 GI2 . By definition of the canonical model, CM1 and CM2 are the only
definitions that add witnesses to concept interpretations. We prove the claim for
the first and include the second in [
G[x;y] 2 S (F 1 ). Since G[x;y] 62 S (F 1 ) the individual is not added. Theorem 2. Let T be an EL -TBox over the set Ncon and Nrole. For every A 2 NcTo;n>, the subsumer sets S (A ) can be computed in polynomial time. Proof Let n = jT j (#GCIs), m = jNconj and i represent each iteration of the subsumer sets s.t S (A ) = Si(A ) once Si(A ) = Si 1(A ) for each A 2 Ncon. The initialisation phase where i = 0 takes m steps to compute - adding > and A to each set S0(A ). For i > 0, the sets Si(A) depend only on Si 1(A ) and GCIs in T . Since jSi(A )j m, there can be at most jSi(A )j m 1 rule applications that can be fired out of the n possible GCIs in T . i is also bounded by m since there can be no more than m iterations, otherwise more than m concepts would have been added to a subsumer set. Computing S (A ) for every A 2 Ncon takes polynomial time w.r.t jT j and jNconj(similarly for each R 2 Nrole).
Although we have the same syntax as ELAL, semantically we capture more information - specifically overlapping intervals - and keep the polynomial time bound without any further extension. There is also room for considering extensions with varying domains, since we adopt a possible world semantics.
Drosophila Development Ontology
The Drosophila Development ontology [
clew_spermatid v spermatid agglomeration_spermatid v spermatid coalescence_spermatid v spermatid
spermatid v 9:partOf:spermatocyte_cyst
We temporalise the ontology as follows. Considering coalescence_spermatid is
at the beginning of the devlopsFrom chain and nothing is contained within this
class and it has no partOf relationships, we label this concept with the the
interval [0; 0], i.e a single stage. The next concept we temporalise is
agglomeration_spermatid. Since the ontology contains the axiom agglom_spermatid
v 9:devlopsF rom:coalescence_spermatid, using similar reasoning to the
labelling of coalescence_spermatid we label agglomeration_spermatid with the
interval [1; 1] . We then replace the first axiom with coalescence_spermatid[0;0] v
agglomeration_spermatid[1;1]. We repeat this process for each axiom of the
form A v 9devlopsF rom:B. We give the class spermatid the interval [
clew_spermatid[2;2] v onion_spermatid[3;3] onion_spermatid[3;3] v leaf blade_spermatid[4;4] leaf blade_spermatid[4;4] v spermatid[0;4]
spermatid[0;4] v 9:partOf[0;4]:spermatocyte_cyst[0;4] We achieve a more succinct and faithful representation by mapping the ontology to an exact time sequence using this temporalisation, and we offer a means to some form of identity across the possible worlds. 6
Summary and Outlook
We presented a new approach for an interval based temporalisation of DLs,
focussing on the lightweight DL EL, based on an AL introduced by Kifer [
We will identify whether varying domains are needed in practise, and if so,
we will investigate the effects of allowing varying domains in EL and see if we
still maintain the polynomial time bound. We also plan to introduce variables
in intervals to indicate some level of uncertainty and to see how closely related,
if at all, this would be when compared with LTL combinations of DLs, namely
LTLEL. We plan to communicate with the authors of the Drosophila
Development Ontology [
173–182 (1987) 24. Wolter, F., Zakharyaschev, M.: On the decidability of description logics with modal operators. In: KR. pp. 512–523 (1998)