=Paper=
{{Paper
|id=Vol-1193/paper_81
|storemode=property
|title=Temporalising EL Concepts with Time Intervals
|pdfUrl=https://ceur-ws.org/Vol-1193/paper_81.pdf
|volume=Vol-1193
|dblpUrl=https://dblp.org/rec/conf/dlog/LeoSP14
}}
==Temporalising EL Concepts with Time Intervals==
https://ceur-ws.org/Vol-1193/paper_81.pdf
Temporalising EL Concepts with Time Intervals
Jared Leo, Bijan Parsia, and Uli Sattler
The University of Manchester
Oxford Road, Manchester, M13 9PL, UK
{jared.leo,bijan.parsia,ulrike.sattler}@manchester.ac.uk
Abstract. 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.
1 Introduction
Description Logics (DLs) [4] are unable to capture simple temporal information
and, as a step towards solving this problem, proposals for adding a tempo-
ral aspect to DLs have been considered. Some proposals [20, 2, 18] suggest the
combination of DLs and Temporal Logics (TLs) [9, 11, 13, 19] to form Temporal
Description Logics (TDLs), where a standard approach, first proposed by Schild
[20], involves the combination of standard DLs, such as ALC [21] with standard
TLs such as Linear Temporal Logic (LTL) [11, 13, 19] to form LTLALC [2, 18].
In this approach, temporal operators from LTL are added to ALC concept de-
scriptions to build temporal statements. Other suggestions include using time
points and intervals based on Allens 13 interval relations [1, 12], those developed
for temporal query answering [7], or temporal data access [6].
Temporal aspects are showing up in numerous ontologies, particularly in
life science and developmental ontologies. The OBO-relation ontology [22] is a
widely used example of this. This ontology incorporates core upper-level relations
such as part of as well as biology-specific relations such as develops from. Time
information is present in all of the informal definitions of the relations. As an
example, consider the definition of the relation located in:
“ 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 [10] which describes
developmental stages of the life cycle of a Drosophila (fruit) fly. Many of its
classes are defined in terms of a chain of develops_from relations that indicates
one stage coming after another, or, one class developing into another at some
specific time point. A sequence of these stages is implicitly given through these
chains. Again, it is clear that temporal information is present here, but more
importantly, very specific time information is present where all time points are
known.
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 appli-
cations 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 rep-
resentation 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 [16] denoted as AL, where we combine the gen-
eral semantics of AL, with EL. We extend the semantics to encode annotation
variables as time intervals to represent time. The second is a more general ap-
proach where we consider using a possible world semantics. With the two new
logics, we hope to provide a more a succinct representation of time for stage
based ontologies.
2 Preliminaries
ELH & EL We assume the reader to be familiar with the syntax and semantics
of ELH and EL [3, 8]. We use an RBox to capture role inclusion axioms, instead
of the traditional method of incorporating these axioms into the TBox. If T is
a TBox, we use Te to be the signature of the TBox, i.e. the subset of Ncon for
which elements are directly used in T , similarly for an ABox A, an RBox R or
a knowledge base K.
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.
Fig. 2. A semilattice of intervals
Fig. 1. An ideal over a semi lattice
3 Introducing ELAL
3.1 Annotated Logics
Annotated Logics (ALs) are formalisms that have been applied to knowledge
representations and expert systems, first introduced in [23] and later studied
in [16, 15, 5]. ALs are also important to consider when incorporating time into
DLs. Instead of combining temporal operators from TLs to concepts, ALs can
‘annotate’ parts of a formulae with time information, at an atomic level. Kifer in
[16] introduced a general semantics for ALs (denoted as AL) based on ideals of
semilattices, where annotations are elements of a semilattice with some ordering
≥ and the least upper bound operator t. Formulae of AL are simply first order
logic formulae where atoms are annotated with elements of a given semilattice.
W.l.o.g., we assume all atoms to be annotated with some lattice element. Next,
we define the semantics of AL as described in [16], but without reference to Her-
brand interpretations. Note that we assume an upper semilattice of annotations
needs not be complete - we only assume the existence of a greatest element.
Definition 1. An ideal ID of a semilattice SL is any subset S s.t.
– s ∈ S and t ≤ s −→ t ∈ S and
– s, t ∈ S −→ s t t ∈ S.
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) ∈ ∆I and (ii) each n-ary predicate symbol P and each tuple
a1 , . . . , an ⊆ (∆I )n to an ideal S ∈ ID(SL). The interpretation is extended to
formulae as follows: let I be a generalized interpretation, ν a valuation, α ∈ SL,
A a ground atom, and F a formula. Then:
1. I, ν |= A(t1 , . . . , tn ) : α if α ∈ I(A(e1 , . . . , en )), where ei = I(ti ) if ti is a
constant and ei = ν(ti ) if ti is a variable,
2. I, ν |= ¬A(t1 , . . . , tn ) : α if ¬(α) ∈ I(A(e1 , . . . , en )) , where ei = I(ti ) if ti
is a constant and ei = ν(ti ) if ti is a variable,
3. I, ν |= F 1 ∧ F 2 if I, ν |= F 1 and I, ν |= F 2 ,
4. I, ν |= ∃x.F if I, ν 0 |= F (x) for some x-variant ν 0 of ν,
5. I, ν |= ∀x.F if I, ν 0 |= F (x) for all x-variants ν 0 of ν.
As usual, I is said to be a model of a formula F if I |= 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 ∈ 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 ∈ SL. The
ordering ≤ is as follows: λ1 < λ2 iff λ1s ≥ λ2s and λ1e ≤ λ2e . Let min(SL) = λs for
0 0 0
λ ∈ SL s.t 6 ∃λ ∈ SL and λs < λs . Let max(SL) = λe for λ ∈ SL s.t 6 ∃λ ∈ SL
0
and λe > λ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. ∀x B[1,1] (x) ⇒ A[1,2] (x)
2. ∀x ∃y A[1,1] (x) ⇒ R[1,3] (x, y) ∧ C[1,2] (y)
3. ∀x ∃y 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 {[1,3], [1,2], [2,3], [1,1]}. Therefore we have, for
any model I of a knowledge base, for any valuation ν, and for any λ ∈ ID([1, 3]):
I, ν |= A[1,3] (x) ⇒ Aλ (x) (1)
We now combine the semantics of AL and EL to form ELAL - our first attempt
at temporalising EL with time intervals based on AL.
3.2 ELAL - The EL fragment of AL
ELAL concept descriptions extend EL concept descriptions with the use of inter-
vals (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, λ ∈ 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 −→ >λ> | Aλ | C u D | ∃Rλ .C
The semantics is given in terms of an interpretation:
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 = C I ∩ DI
– (∃Rλ1 .C)I = {x ∈ ∆I | ∃y ∈ C I ∧ (x, y) ∈ RλI1 }
as well as the following restrictions on the domain reflecting the general seman-
tics from AL:
1. AIλ1 ⊆ AIλ2 ←− λ1 ≥ λ2 and Aλ1 , Aλ2 ∈ Ncon
2. RλI1 ⊆ RλI2 ←− λ1 ≥ λ2 and Rλ1 , Rλ2 ∈ Nrole
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 , ∀x : 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.
3.3 From ELAL to ELH
Reduction We unfold the restrictions on the domain of ELAL into an ELH KB,
similar to the reduction found in [6], according to the following definition:
Definition 5. Let K = (T ,A,SL) be an ELAL KB over the set Ncon and Nrole .
The ELH KB R(K) = (T 0 , A, R) is defined as follows:
n o
T 0 :=T ∪ Aλ1 v Aλ2 | Aλ1 , Aλ2 ∈ Te ∧ λ1 ≥ λ2
n o
R := Rλ1 v Rλ2 | Rλ1 , Rλ2 ∈ Te ∧ λ1 ≥ λ2
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 mod-
els.
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 poly-
nomial time w.r.t |K|.
e
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 [8] that sub-
sumption in ELH can be decided in polynomial time. Therefore, since we have
a polynomial reduction from ELAL into ELH, we can compute subsumption in
ELAL in polynomial time.
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 {[1, 4], [2, 5], [3, 6], [1, 7]}, and a TBox T := {C[1,7] v
A[1,4] u A[3,6] , A[2,5] v D[1,7] }. 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 over-
come these 2 problems, we move towards a new version of an interval based EL
with a possible worlds semantics.
4 ELλ - A Possible World Semantics
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.
4.1 Syntax and Semantics of ELλ
ELλ concept descriptions are built in the same way as ELAL concept descrip-
tions, however the intervals need no longer appear in a semilattice. In ELλ , the
semantics of concept descriptions is defined in terms of a temporal interpreta-
tion with possible worlds. The possible worlds are a finite sequence of normal
EL interpretations indexed by i ∈ 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 ∈ {m, ..., n} ⊆ 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
– >I i = ∆ I
– (C u D)Ii := C Ii ∩ DIi
– (∃R.C)Ii := {e ∈ ∆I | ∃f ∈ C Ii ∧ (e, f ) ∈ RIi }
·I is a global function which maps each labelled concept name A[x,y] to AI[x,y] =
Ii I Ii I
T T
x≤i≤y A , and each role R[x,y] to R[x,y] = x≤i≤y R . The function · is
inductively extended to arbitrary concepts with labelled elements as follows:
– >I = ∆ I
– (C u D)I := C I ∩ DI
– (∃Rλ .C)I := {e ∈ ∆I | ∃f ∈ C I ∧ (e, f ) ∈ RλI }
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 ).
Lemma 3. For any I, (1) AI[x,y] ⊆ AI[u,v] if x ≤ u ≤ v ≤ y. (2) AI[x,y] ∩ AI[u,v] ⊆
AI[m,n] if x < u ≤ y + 1 ≤ v, m ≥ 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 Decision Procedure
As usual, we rely on an ELλ TBox to be in normal form before computing
subsumption.
λ λ
Definition 7. Let T be an ELλ -TBox over the set Ncon and Nrole . T is nor-
malised iff T contains only GCIs of the forms:
Aλ1 v Bλ2
Aλ1 u Bλ2 v Cλ3
Aλ1 v ∃Rλ2 .Bλ3
∃Rλ1 .Aλ2 v Bλ3
λ
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 [3, 8]. We use a similar approach
shown in [8] to transform any ELλ TBox into a normalised version in polynomial
time. Due to space constraints, the transformation proof can be found in [17].
Subsumer Sets We now show how we can compute subsumption relations for
any labelled concept name occurring in an ELλ -TBox. Using a similar approach
λ
to [8], we compute this by building a set S∗ (Aλ ) for every Aλ ∈ Ncon , for which
each set contains labelled concept names that are subsumers of Aλ (similarly for
λ
each Rλ ∈ Nrole ). The subsumer sets are defined as follows:
λ λ
Definition 8. Let T be an ELλ -TBox (normalized) over the set Ncon and Nrole .
λ
For every Aλ ∈ Ncon , and every i ∈ N, the subsumer set Si (Aλ ) is defined in-
ductively by first applying rules INIT0 and INIT1, then for every i ≥ 0, Si+1 (Aλ )
is defined by extending Si (Aλ ) by exhaustive application
S of rules CR0-CR5. The
subsumer set S∗ (Aλ ), defined as the union of i≥0 Si (Aλ ). Si+1 (Aλ ) is com-
plete if no more rules are applicable for any subsumer set (similarly for each
Rλ ∈ Nrole ).
λ
– INIT0 S0 (Aλ ) := {>, Aλ } for every Aλ ∈ Ncon ,
λ
– INIT1 S0 (Rλ ) := {Rλ } for every Rλ ∈ Nrole
– CR0 If A[x,y] ∈ Si (Cλ1 ) and Dλ2 ∈ Si (A[u,v] ) where x ≤ u ≤ v ≤ y and
Dλ2 6∈ Si (Cλ1 ) then Si+1 (Cλ1 ) := Si (Cλ1 ) ∪ {Dλ2 }
– CR1 If Aλ1 v Bλ2 ∈ T and Aλ1 ∈ Si (Cλ3 ) and Bλ2 ∈ / Si (Cλ3 ) then
Si+1 (Cλ3 ) := Si (Cλ3 ) ∪ {Bλ2 }.
– CR2 If Aλ1 u Bλ2 v Cλ3 ∈ T and Aλ1 , Bλ2 ∈ Si (Dλ4 ) and Cλ3 ∈ / Si (Dλ4 )
then Si+1 (Dλ4 ) := Si (Dλ4 ) ∪ {Cλ3 }.
– CR3 If Aλ1 ∈ Si (Bλ2 ) and Aλ1 v ∃Rλ3 .Cλ4 ∈ T and Dλ5 ∈ Si (Cλ4 )
and Pλ6 ∈ Si (Rλ3 ) and ∃Pλ6 .Dλ5 v Eλ7 ∈ T and Eλ7 6∈ Si (Bλ2 ) then
Si+1 (Bλ2 ) := Si (Bλ2 ) ∪ {Eλ7 }.
– CR4 If Bλ1 ∈ Si (C[x,y] ) and C[i,j] ∈ Si (Aλ2 ) and C[k,l] ∈ Si (Aλ2 ) and i <
k ≤ j + 1 ≤ l and x ≥ i and y ≤ l and Bλ1 6∈ Si (Aλ2 ) then Si+1 (Aλ2 ) :=
Si (Aλ2 ) ∪ {Bλ1 }
T
– CR5 If R[x,y] , R[u,v] ∈ Nrole and x ≤ u ≤ v ≤ y and R[u,v] 6∈ Si (R[x,y] ) then
Si+1 (R[x,y] ) := Si (R[x,y] ) ∪ {R[u,v] }
λ λ
Theorem 1. Let T be an ELλ -TBox over the set Ncon and Nrole . For every
λ λ
Fλ1 , Gλ2 ∈ Ncon (or Nrole ), it holds that Gλ2 ∈ S∗ (Fλ1 ) iff T |= 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 [17].
Claim: Gλ2 ∈ S∗ (Fλ1 ) ⇒ T |= 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 ∈ Sn−1 (C[x,y] ) and C[i,j] ∈ Sn−1 (Fλ1 ) and C[k,l] ∈ Sn−1 (Fλ1 ) and i < k ≤
j + 1 ≤ l and x ≥ i and y ≤ l and G[u,v] 6∈ Sn−1 (Fλ1 ). By induction hypothesis
it holds that T |= C[x,y] v Gλ2 , T |= Fλ1 v C[i,j] and T |= Fλ1 v C[k,l] .
From Lemma 1 and Lemma 2, T |= Fλ1 v C[x,y] , therefore by transitivity of
subsumption it holds that T |= Fλ1 v Gλ2 proving the claim.
It suffices to show T |= Fλ1 v Gλ2 ⇒ Gλ2 ∈ S∗ (Fλ1 ). We approach this by
proving the contraposition: Claim: Gλ2 ∈ / S∗ (Fλ1 ) ⇒ T 6|= Fλ1 v Gλ2 where we
build a canonical model I of T with a witness x ∈ FλI1 \ GIλ2 . We construct the
canonical model I according to the following definition:
– CM0 ∆I = {aλ1 | Aλ1 ∈ Ncon λ
}
Ii
– CM1 A = {bλ1 | x ≤ i ≤ y and A[x,y] ∈ S∗ (Bλ1 )}
– CM2 RIi = {(aλ3 , bλ4 ) | x ≤ i ≤ y and Cλ1 v ∃Pλ2 .Bλ4 and Cλ1 ∈ S∗ (Aλ3 )
and R[x,y] ∈ S∗ (Pλ2 )}
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 [17].
– Aλ1 v Bλ2 ∈ T −→ AIλ1 ⊆ BλI2 . Let yλ3 ∈ AIλ1 . By definition of CM1
Aλ1 ∈ S∗ (Yλ3 ). By non-applicability of CR1 Bλ2 ∈ S∗ (Yλ3 ), thus by definition
of CM1 yλ3 ∈ BλI2 .
As we have shown that I is a model of T , it remains to show that FλI1 6⊆ GIλ2 when
Gλ2 6∈ S∗ (Fλ1 ) by finding a witness yλ3 ∈ FλI1 \ GIλ2 . Claim: Gλ2 6∈ S∗ (Fλ1 ) ⇒
FλI1 6⊆ GIλ2 . 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 [17]:
– CM1: Let [x, y] = λ2 . CM1 will only add an individual fλ1 to x≤i≤y GIi if
T
G[x,y] ∈ S∗ (Fλ1 ). Since G[x,y] 6∈ S∗ (Fλ1 ) the individual is not added.
λ λ
Theorem 2. Let T be an ELλ -TBox over the set Ncon and Nrole . For every
T ,>
Aλ ∈ Ncon , the subsumer sets S∗ (Aλ ) can be computed in polynomial time.
λ
Proof Let n = |T | (#GCIs), m = |Ncon | and i represent each iteration of the
λ
subsumer sets s.t S∗ (Aλ ) = Si (Aλ ) once Si (Aλ ) = Si−1 (Aλ ) for each Aλ ∈ 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 |Si (Aλ )| ≤ m, there can be at most |Si (Aλ )|−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λ ∈ Ncon
λ λ
takes polynomial time w.r.t |T | and |Ncon |(similarly for each Rλ ∈ 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 exten-
sions with varying domains, since we adopt a possible world semantics.
5 Drosophila Development Ontology
The Drosophila Development ontology [10] describes developmental stages of
the life cycle of the Drosophila (fruit) fly. The ontology shows temporal patterns
through one of its most used properties devlopsFrom. If we interpret this property
as a stage based relation it is our understanding that an axiom of the form
A v ∃devlopsF rom.B should be interpreted as any instance of B at a time
point (stage), develops into an A at the next time point. Notice that temporal
information is completely qualitative, it only tells us about stages and give no
information on how long each stage lasts or even a relative duration. There is also
another property called partOf which we can also interpret a temporal pattern:
if we have the axioms A v ∃partOf.B and A v ∃partOf.C, then the existence
of A depends on the time points at which both B and C exist. We now take a
small subset of the ontology to demonstrate the expressivity of ELλ . We extract
the subset by starting from the class coalescence_spermatid and include classes
that are connected via a devlopsFrom chain. We also include a class connected
by the partOf property. The resulting ontology is shown below:
agglomeration_spermatid v ∃.devlopsF rom.coalescence_spermatid
clew_spermatid v ∃.devlopsF rom.agglomeration_spermatid
onion_spermatid v ∃.devlopsF rom.clew_spermatid
leaf blade_spermatid v ∃.devlopsF rom.onion_spermatid
leaf blade_spermatid v spermatid
onion_spermatid v spermatid
clew_spermatid v spermatid
agglomeration_spermatid v spermatid
coalescence_spermatid v spermatid
spermatid v ∃.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 agglom-
eration_spermatid. Since the ontology contains the axiom agglom_spermatid
v ∃.devlopsF rom.coalescence_spermatid, using similar reasoning to the la-
belling of coalescence_spermatid we label agglomeration_spermatid with the in-
terval [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 ∃devlopsF rom.B. We give the class spermatid the interval [0,4] since
it must exist during the duration of its subclasses that range from 0 to 4. We give
the partOf relation in the axiom spermatid v ∃.partOf.spermatocyte_cyst the
interval [0, 4] since spermatid has the interval [0, 4] and therefore its parts must
exist at the same time. Since spermatocyte_cyst does not occur in any other
axioms we label this with the same interval. We are left with the ontology:
coalescence_spermatid[0,0] v agglomeration_spermatid[1,1]
agglomeration_spermatid[1,1] v clew_spermatid[2,2]
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 ∃.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 [16]
denoted as AL. Our first attempt, ELAL , saw the combination of EL and AL to
form ELAL which was based on a classical DL model. Our second approach, ELλ ,
extended this using a possible world semantics and overcame some shortcom-
ings of the first. We proved that both logics maintained the same polynomial
time complexity bound for reasoning (subsumption) as EL. We then showed how
ELλ can be used in a life-science oriented example by taking the Drosophila
Development Ontology [10] and converting it into a temporal version.
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 Develop-
ment Ontology [10] to discuss our work, and get feedback on the usefulness of
the logic. We have also currently implemented a preliminary reasoner for ELλ ,
using the OWL API [14], which can be used with OWL 2 where intervals appear
as OWL-annotations on class and role names. This will enable us to view the
performance of reasoning once an example has been fully encoded. Finally, we
hope to extend the possible world semantics to more expressive DLs such as
EL++ [3] and ALC [21].
References
1. Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM
26(11), 832–843 (Nov 1983), http://doi.acm.org/10.1145/182.358434
2. Artale, A., Franconi, E.: A survey of temporal extensions of description logics.
Ann. Math. Artif. Intell. 30(1-4), 171–210 (2000)
3. Baader, F., Brand, S., Lutz, C.: Pushing the el envelope. In: Proc. of IJCAI 2005.
pp. 364–369. Morgan-Kaufmann Publishers (2005)
4. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.
(eds.): The Description Logic Handbook: Theory, Implementation, and Applica-
tions. Cambridge University Press (2003)
5. Baader, F., Knechtel, M., Peñaloza, R.: Context-dependent views to axioms and
consequences of semantic web ontologies. J. Web Sem. 12, 22–40 (2012)
6. Bobillo, F., Straccia, U.: Reasoning with the finitely many-valued lukasiewicz fuzzy
description logic sroiq. Inf. Sci. 181(4), 758–778 (2011)
7. Borgwardt, S., Lippmann, M., Thost, V.: Temporal query answering in dl-lite. In:
Eiter, T., Glimm, B., Kazakov, Y., Krötzsch, M. (eds.) Description Logics. CEUR
Workshop Proceedings, vol. 1014, pp. 80–92. CEUR-WS.org (2013)
8. Brandt, S.: Reasoning in elh w.r.t. general concept inclusion axioms. Tech. rep.
(2004)
9. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state
concurrent systems using temporal logic specifications. ACM Trans. Program.
Lang. Syst. 8(2), 244–263 (Apr 1986), http://doi.acm.org/10.1145/5397.5399
10. Costa, M., Reeve, S., Grumbling, G., Osumi-Sutherland, D.: The drosophila
anatomy ontology. Journal of Biomedical Semantics 4(1), 32 (2013), http:
//www.jbiomedsem.com/content/4/1/32
11. Fisher, M.: An Introduction to Practical Formal Methods Using Temporal Logic.
Wiley (2011), http://books.google.co.uk/books?id=zl6OLZv7d1kC
12. Frasincar, F., Milea, V., Kaymak, U.: towl: Integrating time in owl. In: Virgilio,
R.D., Giunchiglia, F., Tanca, L. (eds.) Semantic Web Information Management,
pp. 225–246. Springer
13. Gabbay, D., Hodkinson, I., Reynolds, M.: Temporal Logic: Mathematical Founda-
tions and Computational Aspects. No. v. 1 in Oxford logic guides, Clarendon Press
(1994), http://books.google.co.uk/books?id=oVEZAQAAIAAJ
14. Horridge, M., Bechhofer, S.: The owl api: A java api for owl ontologies. Semantic
Web 2(1), 11–21 (2011)
15. Kifer, M., Lozinskii, E.L.: Ri: A logic for reasoning with inconsistency. In: LICS.
pp. 253–262. IEEE Computer Society (1989)
16. Kifer, M., Subrahmanian, V.S.: Theory of generalized annotated logic programming
and its applications. J. Log. Program. 12(3&4), 335–367 (1992)
17. Leo, J., Parsia, B., Sattler, U.: Temporalising el concepts with time intervals -
technical report. Tech. Rep. 1, Department of Computer Science, The University
of Manchester, Oxford Road, Manchester, M13 9PL, UK (April 2014), http://
www.cs.man.ac.uk.~leoj/techreportELLambda.pdf
18. Lutz, C., Wolter, F., Zakharyaschev, M.: Temporal description logics: A survey.
In: Demri, S., Jensen, C.S. (eds.) TIME. pp. 3–14. IEEE Computer Society (2008)
19. Pnueli, A.: The temporal logic of programs. In: FOCS. pp. 46–57. IEEE Computer
Society (1977)
20. Schild, K.: Combining terminological logics with tense logic. In: Filgueiras, M.,
Damas, L. (eds.) EPIA. Lecture Notes in Computer Science, vol. 727, pp. 105–120.
Springer (1993)
21. Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with comple-
ments. Artif. Intell. 48(1), 1–26 (1991)
22. Smith, B., Ashburner, M., Rosse, C., Bard, J., Bug, W., Ceusters, W., Goldberg,
L.J., Eilbeck, K., Ireland, A., Mungall, C.J., OBI Consortium, Leontis, N., Rocca-
Serra, P., Ruttenberg, A., Sansone, S.A.A., Scheuermann, R.H., Shah, N., Whetzel,
P.L., Lewis, S.: The OBO Foundry: coordinated evolution of ontologies to support
biomedical data integration. Nature biotechnology 25(11), 1251–1255 (Nov 2007),
http://dx.doi.org/10.1038/nbt1346
23. Subrahmanian, V.S.: On the semantics of quantitative logic programs. In: SLP. pp.
173–182 (1987)
24. Wolter, F., Zakharyaschev, M.: On the decidability of description logics with modal
operators. In: KR. pp. 512–523 (1998)