We consider the logical di erence problem for terminologies that are formulated in the lightweight description logic EL with role inclusions for role hierarchies, transitivity, and right-identity. The main result is that deciding whether two terminologies are logically di erent wrt. a signature can be done in ExpTime, thus it is more di cult than the subsumption problem for this logic but not more di cult than deciding logical di erence without role inclusions. This paper extends the result for EL by Lutz and Wolter [11].
The second ontology T 0 contains the axioms:
then the shared signature would additionally include the symbol Leg. In this case, T does not -entail T 0 anymore.
Logical di erence is a variation of the notion of (deductive) conservative
extensions [
There are several important life science ontologies formulated in lightweight
description logics such as E L or mild extension thereof, e.g., E L with role
inclusion axioms. In particular, role inclusion axioms expressing role hierarchies,
transitive roles, and right-identity are of practical importance, e.g. in medical
terminologies [
The following example illustrates how propagation can be expressed using role inclusions. Take T 00 to be the extension of the ontology T above with the two role inclusion axioms expressing right-identity of the role hasLocation wrt. the role isPartOf and transitivity of isPartOf: hasLocation isPartOf v hasLocation
isPartOf isPartOf v isPartOf The fact that a toe is injured can be expressed as Injury u 9hasLocation.Toe. In a medical context, it might be desirable to propagate a property such as being located at a toe along partonomic properties of the toe. For instance, being located at the toe also means being located at the leg. In the presence of T 00, we can derive that a toe is a part of a leg using the transitivity of isPartOf: Toe v 9isPartOf.Leg. Using the role inclusion axiom for right-identity, we can then derive from a toe injury that also the leg is injured: Injuryu9hasLocation.Leg.
In this paper, we consider ontologies formulated as general TBoxes in the
description logic E L allowing for additional role inclusion axioms of the form
r v s (role hierarchy ), r r v r (transitivity ) and s r v s (right-identity ).
The main result states that the logical di erence problem for such ontologies
can be decided in ExpTime. Thus, this problem is no more complex than for
plain E L, for which it was shown to be ExpTime-complete [
The presented decision procedure decides non- -entailment by searching for
the existence of a concept inclusion witnessing the logical di erence between the
input ontologies. We show that it is su cient to only search for a succinct
representation of a concept that occurs at the left-hand side of such concept inclusions.
Then, the ontologies are logically di erent if, and only if, such a representation
of a concept was found. Computing a list of logical di erences between
ontologies, however, is a harder problem. As it was observed in [
The paper is organized as follows. We start with de ning E L with role inclusions in the next section. In Section 3, we state the de nitions for the notions of logical di erence and -entailment and present some illustrating examples. In Section 4, we describe canonical models for E L with role inclusions and simulation relations between them. Then these notions will be used to give a characterization of -entailment for constraint boxes in Section 5. The algorithm deciding non- -entailment in exponential time is presented in Section 6 together with an example. The nal section concludes this paper.
The algorithm described in this paper is based on and described along the
lines of the algorithm deciding conservative extensions in E L [
We begin with introducing the description logic E L. Let NC and NR be two countably in nite and disjoint sets of concept names and role names, respectively. E L-concepts are build according to this syntax rule:
C ::= > j A j C u D j 9r:C; where A ranges over the concept names in NC, r over role names in NR, and C; D over E L-concepts. The semantics of E L is de ned by means of interpretations I = ( I ; I ), where the interpretation domain I is a non-empty set, and I is a function mapping each concept name A to a subset AI of I , and each role name rI to a binary relation rI I I . The function I is inductively extended to arbitrary concepts by setting >I := I , (C u D)I := CI \ DI , and (9r:C)I := fd 2 I j there is an e 2 I such that (d; e) 2 rI and e 2 CI g.
A terminology (TBox) is a nite set of concept inclusions (CIs) C v D, where C and D are concepts. An interpretation I satis es a CI C v D, written I j= C v D, if, and only if, CI DI . I is a model of a TBox T if, and only if, it satis es all CIs in T . We write T j= C v D if, and only if, every model of T satis es C v D.
In this paper, we consider an extension of E L with role inclusions (RIs) of the form r v s, r r v r or r s v r, where r; s are roles. A role box (RBox) is a nite set of RIs. An interpretation I satis es an RI r v s (r r v r, r s v r), written I j= r v s (I j= r r v r, I j= r s v r), if, and only if, rI sI (rI rI rI , rI sI rI ). We interpret the role operator ` ' as the composition of binary relations, i.e., R S = f(d; d00) j there exists a d0 such that dRd0 and d0Sd00g, for binary relations R and S. I is a model of an RBox R if, and only if, it satis es all RIs in R. We write R j= r v s (R j= C v D) if, and only if, every model of R satis es the RI r v s (the CI C v D). A constraint box (CBox) C = (T ; R) consists of a TBox T and an RBox R. An interpretation I is a model of a CBox C = (T ; R) if, and only if, I is a model of both T and R. We write C j= C v D if, and only if, every model of C satis es C v D.
A signature is a nite subset of NC [ NR. The signature sig(X) is the set of concept and role names which occur in X, where X ranges over concepts C, CIs C v D, RIs r v s, TBoxes T , RBoxes R, and CBoxes C. If sig(C) , we also call C a -concept. 3
We de ne the notion of -entailment in terms of logical di erence wrt. a signature for CBoxes.
De nition 1 ( -di erence, -entailment). The C0 is de ned as -di erence between C and Di (C; C0) = fC v D j C 6j= C v D, C0 j= C v D, and sig(C v D) [ Di (R; R0): g C -entails C0, in short C v
C0, if, and only if, Di (C; C0) = ;.
The following two examples illustrate these notions and their relation to each other.
Example 1. Let = fA; r; sg be a signature, C = (T ; R) and C0 = (T 0; R0) be two CBoxes, where T = f> v 9r:Ag, R = ;, T 0 = f> v 9r:B; 9s:B v Ag, and R0 = fr v sg. It can easily be seen that T -entails T 0 and R does not -entail R0. But, when combining the TBoxes with the RBoxes, this yields that C does not -entail C0. The concept inclusion > v A 2 Di (C; C0) witnesses the logical di erence between C and C0 wrt. . a Example 2. Let = fs; s0g be a signature, and C = (T ; R) and C0 = (T 0; R0) be two CBoxes, where T = ;, R = fs v s0g, T 0 = f> v 9r:>g, and R0 = fr v sg. Then we have that T -entails T 0, and R -entails R0. However, observe that C does not -entail C0. The logical di erence wrt. between C and C0 is witnessed by the concept inclusion > v 9s:> 2 Di (C; C0). a
As already mentioned in the introduction, the CIs witnessing the logical
di erence between CBoxes even without role inclusion axioms can be very large.
More precisely, Di (C; C0), where the RBoxes in C; C0 are empty, can contain
CIs of at least doubly exponential size; see [
In the remainder of this paper, we investigate the complexity of deciding the problem: Given two CBoxes C, C0 and a signature , does C -entail C0? We restrict ourselves to sig(C0). 4
In this section, we construct canonical models for E L with role inclusions and describe relations between canonical models using a simulation relation. De nition 2 ( -Simulation). Let I1 and I2 be interpretations and a signature. A relation S I1 I2 is a -simulation from I1 to I2 if the following holds: { for all concept names A 2 and all (d1; d2) 2 S with d1 2 AI1 , d2 2 AI2 ; { for all role names r 2 , all (d1; d2) 2 S, and all e1 2 I1 with (d1; e1) 2 rI1 , there exists e2 2 I2 such that (d2; e2) 2 rI2 and (e1; e2) 2 S. If d1 2 I1 ; d2 2 I2 , and there is an -simulation S from I1 to I2 with (d1; d2) 2 S, then (I2; d2) -simulates (I1; d1), written (I1; d1) (I2; d2). If = NC [ NR, we write ` ' instead of ` '.
Let I be an interpretation, a signature, and d 2 I . We de ne the abbreviation d ;I := fC j d 2 CI and sig(C) g. The outdegree of an interpretation I is the the maximum number of role successors at any point in its domain and for any role in NR. Formally, the outdegree of I is maxfjfd0 2 I j (d; d0) 2 rI gj : d 2 I ; r 2 NRg.
The following characterization of -simulation establishes a connection
between -simulation and -concepts. The proof is standard; see, e.g., [
We use sub(C) and sub(T ) to denote the set of subconcepts of a concept C and the set of subconcepts occurring in the TBox T , respectively. De nition 3 (Canonical model). Let C = (T ; R) be a CBox, and D a concept. The canonical model ID;C = ( ID;C ; ID;C ) is de ned as follows: {
ID;C = fDg [ fC j 9r:C 2 sub(D) [ sub(T )g; { C 2 AID;C i C j= C v A; for all A 2 NC; { (C; C0) 2 rID;C i one of the following holds: (a) C j= C v 9r:C0 and C0 2 sub(T ), (b) R j= C v 9r:C0 and C0 2 sub(C).
The model ID;C can be constructed in polynomial time in the size of C and D
as subsumption wrt. CBoxes in EL can be decided in polynomial time [
Foot hasLocation
isPartOf hasLocation
Fig. 1. The canonical model ID;C.
The following lemma summarizes the relevant properties of canonical models.
It extends similar lemmas for EL in [
The closure cl(C; D) of a CBox C = (T ; R) and a concept D is the smallest set such that: { sub(T ) cl(C; D); { sub(D) cl(C; D); { if 9r:C 2 cl(C; D) and r v s 2 R, then 9s:C 2 cl(C; D); { if 9r:C 2 cl(C; D), 9s:C0 2 cl(C; C), and r s v t 2 R, then 9t:C0 2 cl(C; D). We use cl(C) to denote the closure that satis es the rst and the last conditions. Lemma 1 (Properties of canonical models). Let C = (T ; R) be a CBox and C a concept. Then the following holds: 1. IC;C is a model of C. 2. For all D 2 IC;C and all E 2 cl(C; C), we have D 2 EIC;C i C j= D v E. 3. For all models I of C and all d 2 I , the following conditions are equivalent: (a) d 2 CI ; (b) (IC;C; C) (I; d). 4. The following conditions are equivalent: (a) C j= C v D; (b) C 2 DIC;C ; (c) (ID;C; D) (IC;C; C). 5. If 9r:D 2 cl(C; Ci) for all i 2 f1; 2g, then (IC1;C; D) (IC2;C; D).
In this section, we provide a characterization of -entailment wrt. CBoxes in
terms of canonical models. The lemmas are extensions of their E L-counterparts
in [
We rst consider an auxiliary lemma, which we need for proving Lemma 4 below.
Lemma 2. Let C = (T ; R) be a CBox. Suppose C j= C v 9r:D. Then one of the following holds: (a) there exists a C0 2 sub(T ) such that C j= C v 9r:C0 and C j= C0 v D; (b) there exists a C0 2 sub(C) such that R j= C v 9r:C0 and C j= C0 v D. Example 4. We illustrate the cases in Lemma 2. Intuitively, the distinction is between two cases of how a concept in the context of a CBox can enforce a role successor: (i) using TBox axioms; or (ii) without the TBox. For the former case, let C = (T ; R) be a CBox with T = fA v 9s:B; B v B0g and R = fr s v rg. Suppose C j= 9r:A v 9r:B0. For this entailment, only Case (a) applies: we have that C j= 9r:A v 9r:B, C j= B v B0, and B 2 sub(T ). In other words, the concept 9r:A triggers the TBox axiom A v 9s:B which implies 9r:9s:B. Using the right-identity rule in R, we get 9r:B. Then, from the CI B v B0, it follows that 9r:B0.
Consider (ii). Let C = (T ; R) with T = fA v B0g and R = fr s v rg. Suppose C j= C v 9r:B0, where C = 9r:9s:(A u B). Here, Case (b) applies: it holds that R j= C v 9r:(A u B), C j= A u B v B0, and A u B 2 sub(C). Intuitively, C itself enforces a role path of length two without utilizing CIs from T . The path is then abbreviated by R. Finally, the TBox axiom together with 9r:(A u B) implies 9r:B0. a
The following lemma is essential for characterizing -entailment. Intuitively, it states that, given an arbitrary large concept C, we can always nd a possibly shorter concept with bounded outdegree that expresses the same \relevant" information. What information is considered relevant, is made precise by a set of consequences KC(D) of a concept D in the presence of a CBox C. We are interested in those consequences that are concepts of the closure cl(C; D).
The set KC(D) is given as:
KC(D) = fE 2 cl(C; E) j C j= D v Eg: Lemma 3 (Bounded outdegree). For all CBoxes C = (T ; R) and concepts C, there is a concept D such that the following conditions are satis ed: 1. ; j= C v D; 2. KC(C) = KC(D); 3. jDj jCj; 4. the outdegree of D is bounded by jCj.
For the following characterization of -entailment, we use a relation `)1' on concepts. Let C1; C2 be CBoxes, C a -concept, and D a sig(C2)-concept. We write C )1 D if, and only if, for all -concepts E, C2 j= D v E implies C1 j= C v E.
Lemma 4 (Characterization of non- -entailment). Let C1 = (T1; R1) and C2 = (T2; R2) be two CBoxes, and sig(C2) a signature. Then Di (C1; C2) 6= ; if, and only if, there is a -concept C and a sig(C2)-concept D 2 cl(C2) such that: (a) C2 j= C v D; (b) C 6)1 D; (c) the outdegree of C is bounded by jC2j.
The next lemma characterizes the relation `)1' semantically in terms of simulation between canonical models. Moreover, it states that membership in `)1' can be decided in polynomial time.
Lemma 5 (Semantic characterization). Let C1; C2 be CBoxes and C; D concepts. Then we have C )1 D if, and only if, (ID;C2 ; D) (IC;C1 ; C). Hence, the problem C )1 D is decidable in polynomial time in the size of C; D, and C2. 6
We present an algorithm for deciding -entailment for EL with role inclusions. To check whether C1 v C2, the algorithm searches for a -concept C such that for some D 2 sub(T2), the Points (a){(c) of Lemma 4 are satis ed. The algorithm proceeds in rounds. In the rst round, Points (a) and (b) are checked for all conjunctions C of concept names from and all D 2 sub(T2). Each check can be done in polynomial time by Lemma 5. In case, no suitable C is found in round one, the algorithm proceeds to the second round in which concepts C of role depth one are considered. Here C is a conjunction of concept names from and concepts of the form 9r:E, where r is a role from and E is a candidate for C from the previous round, i.e., E is a conjunction of concept names. By Point (c) of Lemma 4, we only have to consider those Cs with no more than jT2j many conjuncts of the form 9r:E. For checking Points (a) and (b), we make use of the information we have gained about the Es in the previous round. If still no suitable C is found, the algorithm starts round three that checks concepts C of role depth two in which we reuse the Cs from the second round as role successors. If again no suitable concept C was found, the algorithm proceeds to the next round, etc.
To avoid constructing doubly exponentially large concepts C, the algorithm uses a succinct data structure that represents the relevant information about C. Which information about C is relevant can be read of the characterization of -entailment in Lemma 4: For every C, take the quintuple
C] = (Q0; Q1; Q2; Q3; Q4); where the set Q0 contains all concept names occurring in the top-level conjunction of C,
Q1 = KC1 (C); Q2 = KC2 (C); Q3 = f(r; D0) 2 ( \ NR) sub(T2) j C0 )1 D0 and
C1 j= C v 9r:C0g; and
Q4 = fD 2 sub(T2) j C )1 Dg: The quintuple C] is said to be determined by C. Intuitively, the components Q1 and Q2 contain concepts that are implied by C in the context of C1 and C2, respectively, and Q4 contains concepts which, while being in the context of C2, can be -simulated by C in the context of C1.
According to Lemma 4, the quintuple C] determined by a concept C contains su cient information to decide whether C is the left-hand side of a CI witnessing the logical di erence between two CBoxes. Moreover, the information in C] enables the recursive search described above and to formulate a termination condition for the algorithm to run in exponential time.
Figure 2 presents the algorithm for deciding -entailment for EL with role inclusions. Observe that the termination condition Q2 n Q4 6= ; corresponds to satisfaction of Points (a) and (b) in Lemma 4. Note that Point (a) in the de nition of the set F3 uses canonical models, which are constructed on demand in polynomial time.
Notice that, in Figure 2, we use a binary auxiliary relation vrRh on roles for an RBox R such that r vrRh s if, and only if, r v s 2 R. Let vR rh be the re exive, rh. transitive closure of vR Example 5. We illustrates the algorithm in Figure 2 by computing an answer to the question `Does C1 = fT ; ;g -entail C2 = fT ; Rg?', where T and R are as in Example 3 in Section 4. In Step 1, the algorithm computes the quintuples in the set N0. For instance, the quintuple qToe 2 N0 determined by the concept name Toe. We have qToe = (Q0; Q1; Q2; Q3; Q4), where
Q4 = Q2: Q0 = fToeg; Q1 = fToe; 9isPartOf:Footg; Q2 = Q1;
Q3 = f(isPartOf; Foot); (isPartOf; 9isPartOf:Leg)g; In Step 2, the algorithm checks whether Q2 n Q4 6= ;. As this is not the case, it proceeds with Step 3 by computing the set N00 of quintuples, each from a set F0 of concept names from and a set Q of pairs of a -role and a quintuple from N0. Let F0 = ; and Q = f(hasLocation; qToe)g. The algorithm computes the quintuple qD determined by the concept D:
D = l A u l
9r:( l D) : Input: CBoxes C1 = (T1; R1) and C2 = (T2; R2) and signature sig(C2). (i) D 2 Q4 and s vrRh1 r; or (ii) (t; D) 2 Q3, s vrRh1 r1, t vrRh1 r2, and r1 r2 v r 2 R1 ; { F4 =
D 2 cl(C2) j (a) for all A 2 (b) for all r 2 , A 2 KC2 (D) implies A 2 F1; and , (D; D0) 2 rID;C2 implies (r; D0) 2 F3 .
This is done until Ni contains a quintuple (Q0; Q1; Q2; Q3; Q4) such that Q2 nQ4 6= ;, or Ni+1 = Ni. Output `C1 6v C2' if the rst condition applies; otherwise, output `C1 v C2'. That is, D = D1 u D2, where D1 = 9hasLocation:Toe and D2 = 9hasLocation: 9isPartOf:Foot. Then qD = (F0; F1; F2; F3; F4) is computed from F0 and Q, where:
F1 = fD; D1; D2g; F2 = F1 [ f9hasLocation:Foot; 9hasLocation:Legg; F3 = f(hasLocation; Toe); (hasLocation; 9isPartOf:Footg;
F4 = ;: The algorithm terminates and outputs `C1 6v C2' since F2 n F4 6= ;.
a
Before we continue to show correctness of the algorithm, we explicitly state
the concepts that determine the quintuples constructed in Step 3 of Figure 2.
Lemma 6. Let (F0; F1; F2; F3; F4) be the quintuple computed from F0 and Q in
Figure 2. For each (r; q) 2 Q, let Cr;q be the concept which determines the
quintuple q. Then C = dA2F0 A u d(r;q)2Q 9r:Cr;q determines (F0; F1; F2; F3; F4).
This lemma extends a similar lemma in [
Finally, we show correctness and complexity of the algorithm in Figure 2.
The proof is similar to the one for the corresponding theorem in [
Proof. Soundness follows from Lemmas 4 and 6. For completeness, assume C v D 2 Di (C1; C2). By Lemma 4, C is of outdegree bounded by jC2j and D 2 sub(T2) such that C2 j= C v D and C 6)1 D. If C is a conjunction of concept names, then the algorithm outputs `C1 6v C2' in Step 2. Suppose C has role depth n 1. One can show by induction on i using Lemma 6 that, for all i 0, the set Ni contains all quintuples determined by subconcepts C0 of C of role depth smaller than i. Hence, after computing the set Ni for some i n, the algorithm outputs `C1 6v C2'.
For termination and time complexity consider the following. To see that Steps 1 and 2 of the algorithm run in polynomial time notice that, by Lemma 5, the algorithm can compute any quintuple determined by a conjunction of concept names from in polynomial time. Consider Step 3. For each quintuple (Q0; Q1; Q2; Q3; Q4), we have Q0 and Qi cl(C2), for 1 i 4. That is, the total number of possible quintuples is bounded by 25jC2j. Consequently, the algorithm terminates since Nj = Nj+1, for some j 25jC2j. For showing that the algorithm runs in exponential time, we now show that Ni+1 can be computed from Ni in exponential time. The number of pairs (F0; Q) in Figure 2, where F0 \ NC and Q ( \ NR) Ni with jQj jC2j, is exponential in jC2j. Moreover, given a pair (F0; Q), computing the quintuple (F0; F1; F2; F3; F4) in Figure 2 only takes polynomial time in jC2j. tu 7
We have shown that deciding -entailment in E L with role inclusions for role
hierarchy (r v s), transitivity (r r v r), and right-identity (s r v s) is
ExpTime-complete. These forms of role inclusion axioms have been argued to
be of practical importance, e.g., in medical terminologies [
For future work, it is interesting to extend the presented algorithmic framework to capture more expressivity by, e.g., allowing for more role inclusions, inverse roles, universal roles, nominals, etc.