Deciding the logical difference problem for EL with role inclusions Daniel Pokrywczynski and Dirk Walther University of Liverpool, UK Abstract. We consider the logical difference problem for terminologies that are formulated in the lightweight description logic EL with role in- clusions for role hierarchies, transitivity, and right-identity. The main result is that deciding whether two terminologies are logically different wrt. a signature can be done in ExpTime, thus it is more difficult than the subsumption problem for this logic but not more difficult than de- ciding logical difference without role inclusions. This paper extends the result for EL by Lutz and Wolter [11]. 1 Introduction While computing the syntactic difference of text files is indispensable, computing the syntactic difference between ontologies consisting of axioms is hardly useful as observed in [12]. When comparing distinct ontologies logically, one should take into account their signatures, as the interesting differences between ontologies are formulated in their shared signature. The notion of logical difference is based on logical entailment wrt. a signature [9]: an ontology T Σ-entails an ontology T 0 for a signature Σ if, for all concept implications C v D formulated in Σ, we have that T 0 |= C v D implies T |= C v D. In case both ontologies, T and T 0 , Σ-entail each other, we call them Σ-inseparable. When taking Σ to contain all shared symbols of two ontologies, the ontologies being Σ-inseparable means that they are not logically different. We illustrate Σ-entailment with a simple example formulated in the descrip- tion logic EL. The first ontology T consists of the following two axioms: Toe v ∃isPartOf.Foot Foot v ∃isPartOf.Leg The second ontology T 0 contains the axioms: ToeNail v ∃isPartOf.Toe Toe v ∃isPartOf.Foot The shared signature Σ of T and T 0 is Σ = {Toe, Foot, isPartOf}. We have that T Σ-entails T 0 , but not vice versa. If we extend T 0 to include the axiom: ∃isPartOf.Foot v ∃isPartOf.Leg then the shared signature Σ would additionally include the symbol Leg. In this case, T does not Σ-entail T 0 anymore. Logical difference is a variation of the notion of (deductive) conservative extensions [5]. More precisely, for two ontologies T ⊆ T 0 and a signature Σ, we have that T Σ-entails T 0 if, and only if, T 0 is a conservative extension of T wrt. Σ. Conservative extensions are an important notion in ontology design and integration. In particular, conservative extensions can be used to formalize independent modules inside an ontology [6, 10]. There are several important life science ontologies formulated in lightweight description logics such as EL or mild extension thereof, e.g., EL with role in- clusion axioms. In particular, role inclusion axioms expressing role hierarchies, transitive roles, and right-identity are of practical importance, e.g. in medical terminologies [8, 16]. For instance, right-identity axioms have been proven useful for expressing “propagation” of one property along another one. An example of a large ontology deploying role inclusion axioms is the Systematized Nomenclature of Medicine, Clinical Terms (Snomed ct), which contains ∼0.4 million axioms and underlies the systematized medical terminology used in health systems of the US, the UK, and other countries [16]. This ontology consists of an acyclic EL-terminology with role hierarchy, right-identity but no transitive roles. Other ontologies which have large parts formulated in EL with role inclusions are the National Cancer Institute (NCI) Ontology [15], the Gene Ontology (GO) [17], which uses a single transitive role ‘part of’, and the Galen Common Reference Model [14], which can be expressed in an extension of EL with functional and in- verse roles [7]. One of the reasons why EL and its extensions are quite appealing as ontology languages is that reasoning is tractable [1, 2]. 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 ∃hasLocation.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 ∃isPartOf.Leg. Using the role inclusion axiom for right-identity, we can then derive from a toe injury that also the leg is injured: Injuryu∃hasLocation.Leg. In this paper, we consider ontologies formulated as general TBoxes in the description logic EL 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 difference problem for such ontologies can be decided in ExpTime. Thus, this problem is no more complex than for plain EL, for which it was shown to be ExpTime-complete [11]. For comparison, the computational complexity of Σ-entailment is 2ExpTime-complete for more expressive description logics such as ALC, ALCQ, and ALCQI [5, 10], but even in such simple formalisms as acyclic propositional Horn Logic deciding logical difference is co-NP-complete [4]. In contrast, the satisfiability problem for EL with the role inclusions mentioned above was shown to be decidable in poly- nomial time [1], and ALCQI satisfiability relative to TBoxes is decidable in ExpTime [18]. Thus, for these logics, deciding logical difference is by at least one exponential harder than satisfiability. The presented decision procedure decides non-Σ-entailment by searching for the existence of a concept inclusion witnessing the logical difference between the input ontologies. We show that it is sufficient to only search for a succinct repre- sentation of a concept that occurs at the left-hand side of such concept inclusions. Then, the ontologies are logically different if, and only if, such a representation of a concept was found. Computing a list of logical differences between ontolo- gies, however, is a harder problem. As it was observed in [11], concept inclusions witnessing logical differences can be of at least doubly exponential size even for EL ontologies without role inclusion axioms. When placing some restrictions on the considered EL ontologies, the computational complexity of computing logical differences can be reduced to tractable as it is shown in [9]. The paper is organized as follows. We start with defining EL with role inclu- sions in the next section. In Section 3, we state the definitions for the notions of logical difference and Σ-entailment and present some illustrating examples. In Section 4, we describe canonical models for EL with role inclusions and simula- tion relations between them. Then these notions will be used to give a character- ization 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 final 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 EL [11]. Due to space restrictions most proofs are omitted; full proofs can be found in [13]. 2 Preliminaries We begin with introducing the description logic EL. Let NC and NR be two countably infinite and disjoint sets of concept names and role names, respectively. EL-concepts are build according to this syntax rule: C ::= > | A | C u D | ∃r.C, where A ranges over the concept names in NC , r over role names in NR , and C, D over EL-concepts. The semantics of EL is defined 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 := C I ∩ DI , and (∃r.C)I := {d ∈ ∆I | there is an e ∈ ∆I such that (d, e) ∈ rI and e ∈ C I }. A terminology (TBox) is a finite set of concept inclusions (CIs) C v D, where C and D are concepts. An interpretation I satisfies a CI C v D, written I |= C v D, if, and only if, C I ⊆ DI . I is a model of a TBox T if, and only if, it satisfies all CIs in T . We write T |= C v D if, and only if, every model of T satisfies C v D. In this paper, we consider an extension of EL 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 finite set of RIs. An interpretation I satisfies an RI r v s (r ◦ r v r, r ◦ s v r), written I |= r v s (I |= r ◦ r v r, I |= 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 = {(d, d00 ) | there exists a d0 such that dRd0 and d0 Sd00 }, for binary relations R and S. I is a model of an RBox R if, and only if, it satisfies all RIs in R. We write R |= r v s (R |= C v D) if, and only if, every model of R satisfies 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 |= C v D if, and only if, every model of C satisfies C v D. A signature Σ is a finite 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 Logical difference We define the notion of Σ-entailment in terms of logical difference wrt. a signa- ture Σ for CBoxes. Definition 1 (Σ-difference, Σ-entailment). The Σ-difference between C and C 0 is defined as Diff Σ (C, C 0 ) = {C v D | C 6|= C v D, C 0 |= C v D, and sig(C v D) ⊆ Σ} ∪ Diff Σ (R, R0 ). C Σ-entails C 0 , in short C vΣ C 0 , if, and only if, Diff Σ (C, C 0 ) = ∅. The following two examples illustrate these notions and their relation to each other. Example 1. Let Σ = {A, r, s} be a signature, C = (T , R) and C 0 = (T 0 , R0 ) be two CBoxes, where T = {> v ∃r.A}, R = ∅, T 0 = {> v ∃r.B, ∃s.B v A}, and R0 = {r v s}. 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 C 0 . The concept inclusion > v A ∈ Diff Σ (C, C 0 ) witnesses the logical difference between C and C 0 wrt. Σ. a Example 2. Let Σ = {s, s0 } be a signature, and C = (T , R) and C 0 = (T 0 , R0 ) be two CBoxes, where T = ∅, R = {s v s0 }, T 0 = {> v ∃r.>}, and R0 = {r v s}. Then we have that T Σ-entails T 0 , and R Σ-entails R0 . However, observe that C does not Σ-entail C 0 . The logical difference wrt. Σ between C and C 0 is witnessed by the concept inclusion > v ∃s.> ∈ Diff Σ (C, C 0 ). a As already mentioned in the introduction, the CIs witnessing the logical difference between CBoxes even without role inclusion axioms can be very large. More precisely, Diff Σ (C, C 0 ), where the RBoxes in C, C 0 are empty, can contain CIs of at least doubly exponential size; see [11] for an example. In the remainder of this paper, we investigate the complexity of deciding the problem: Given two CBoxes C, C 0 and a signature Σ, does C Σ-entail C 0 ? We restrict ourselves to Σ ⊆ sig(C 0 ). 4 Canonical models and simulation relations In this section, we construct canonical models for EL with role inclusions and describe relations between canonical models using a simulation relation. Definition 2 (Σ-Simulation). Let I1 and I2 be interpretations and Σ a sig- nature. A relation S ⊆ ∆I1 ×∆I2 is a Σ-simulation from I1 to I2 if the following holds: – for all concept names A ∈ Σ and all (d1 , d2 ) ∈ S with d1 ∈ AI1 , d2 ∈ AI2 ; – for all role names r ∈ Σ, all (d1 , d2 ) ∈ S, and all e1 ∈ ∆I1 with (d1 , e1 ) ∈ rI1 , there exists e2 ∈ ∆I2 such that (d2 , e2 ) ∈ rI2 and (e1 , e2 ) ∈ S. If d1 ∈ ∆I1 , d2 ∈ ∆I2 , and there is an Σ-simulation S from I1 to I2 with (d1 , d2 ) ∈ 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 ∈ ∆I . We define the abbrevi- ation dΣ,I := {C | d ∈ C I and sig(C) ⊆ Σ}. 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 max{|{d0 ∈ ∆I | (d, d0 ) ∈ rI }| : d ∈ ∆I , r ∈ NR }. The following characterization of Σ-simulation establishes a connection be- tween Σ-simulation and Σ-concepts. The proof is standard; see, e.g., [3]. Theorem 1 (Characterization of Σ-simulation). If (I1 , d1 ) ≤Σ (I2 , d2 ), then dΣ,I 1 1 ⊆ dΣ,I 2 2 . Conversely, if I1 , I2 have finite out-degree, and d1Σ,I1 ⊆ Σ,I2 d2 , then (I1 , d1 ) ≤Σ (I2 , d2 ). 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. Definition 3 (Canonical model). Let C = (T , R) be a CBox, and D a con- cept. The canonical model ID,C = (∆ID,C , ·ID,C ) is defined as follows: – ∆ID,C = {D} ∪ {C | ∃r.C ∈ sub(D) ∪ sub(T )}; – C ∈ AID,C iff C |= C v A, for all A ∈ NC ; – (C, C 0 ) ∈ rID,C iff one of the following holds: (a) C |= C v ∃r.C 0 and C 0 ∈ sub(T ), (b) R |= C v ∃r.C 0 and C 0 ∈ 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 [1]. Example 3. For an illustration of canonical models, recall the TBox T = {Toe v ∃isPartOf.Foot, Foot v ∃isPartOf.Leg} from the introduction together with the RBox R = {hasLocation ◦ isPartOf v hasLocation}. Figure 1 shows the canonical model ID,C , where D = ∃hasLocation.Toe and C = (T , R). a Toe isPartOf Foot isPartOf Leg hasL hasLocation n o catio o catio n hasL ∃hasLocation.Toe Fig. 1. The canonical model ID,C . The following lemma summarizes the relevant properties of canonical models. It extends similar lemmas for EL in [11] and it can be proven analogously. To account for the additional role inclusions, we deploy the following notion of a closure. 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 ∃r.C ∈ cl(C, D) and r v s ∈ R, then ∃s.C ∈ cl(C, D); – if ∃r.C ∈ cl(C, D), ∃s.C 0 ∈ cl(C, C), and r ◦ s v t ∈ R, then ∃t.C 0 ∈ cl(C, D). We use cl(C) to denote the closure that satisfies the first 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 ∈ ∆IC,C and all E ∈ cl(C, C), we have D ∈ E IC,C iff C |= D v E. 3. For all models I of C and all d ∈ ∆I , the following conditions are equivalent: (a) d ∈ C I ; (b) (IC,C , C) ≤ (I, d). 4. The following conditions are equivalent: (a) C |= C v D; (b) C ∈ DIC,C ; (c) (ID,C , D) ≤ (IC,C , C). 5. If ∃r.D ∈ cl(C, Ci ) for all i ∈ {1, 2}, then (IC1 ,C , D) ≤ (IC2 ,C , D). 5 Characterization of Σ-entailment In this section, we provide a characterization of Σ-entailment wrt. CBoxes in terms of canonical models. The lemmas are extensions of their EL-counterparts in [11]. They account for the additional role inclusion axioms, but they can be proven in a similar way. We first consider an auxiliary lemma, which we need for proving Lemma 4 below. Lemma 2. Let C = (T , R) be a CBox. Suppose C |= C v ∃r.D. Then one of the following holds: (a) there exists a C 0 ∈ sub(T ) such that C |= C v ∃r.C 0 and C |= C 0 v D; (b) there exists a C 0 ∈ sub(C) such that R |= C v ∃r.C 0 and C |= C 0 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 = {A v ∃s.B, B v B 0 } and R = {r ◦ s v r}. Suppose C |= ∃r.A v ∃r.B 0 . For this entailment, only Case (a) applies: we have that C |= ∃r.A v ∃r.B, C |= B v B 0 , and B ∈ sub(T ). In other words, the concept ∃r.A triggers the TBox axiom A v ∃s.B which implies ∃r.∃s.B. Using the right-identity rule in R, we get ∃r.B. Then, from the CI B v B 0 , it follows that ∃r.B 0 . Consider (ii). Let C = (T , R) with T = {A v B 0 } and R = {r ◦ s v r}. Suppose C |= C v ∃r.B 0 , where C = ∃r.∃s.(A u B). Here, Case (b) applies: it holds that R |= C v ∃r.(A u B), C |= A u B v B 0 , and A u B ∈ 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 ∃r.(A u B) implies ∃r.B 0 . a The following lemma is essential for characterizing Σ-entailment. Intuitively, it states that, given an arbitrary large concept C, we can always find a possi- bly 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) = {E ∈ cl(C, E) | C |= D v E}. Lemma 3 (Bounded outdegree). For all CBoxes C = (T , R) and concepts C, there is a concept D such that the following conditions are satisfied: 1. ∅ |= C v D; 2. KC (C) = KC (D); 3. |D| ≤ |C|; 4. the outdegree of D is bounded by |C|. 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 |= D v E implies C1 |= 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 Diff Σ (C1 , C2 ) 6= ∅ if, and only if, there is a Σ-concept C and a sig(C2 )-concept D ∈ cl(C2 ) such that: (a) C2 |= C v D; (b) C 6⇒1 D; (c) the outdegree of C is bounded by |C2 |. 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 con- cepts. 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 Algorithm 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 ∈ sub(T2 ), the Points (a)–(c) of Lemma 4 are satisfied. The algorithm proceeds in rounds. In the first round, Points (a) and (b) are checked for all conjunctions C of concept names from Σ and all D ∈ 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 ∃r.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 |T2 | many conjuncts of the form ∃r.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 conjunc- tion of C, Q1 = KC1 (C), Q2 = KC2 (C), Q3 = {(r, D0 ) ∈ (Σ ∩ NR ) × sub(T2 ) | C 0 ⇒1 D0 and C1 |= C v ∃r.C 0 }, and Q4 = {D ∈ sub(T2 ) | C ⇒1 D}. 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 sufficient information to decide whether C is the left-hand side of a CI witnessing the logical difference 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 \ Q4 6= ∅ corresponds to satisfaction of Points (a) and (b) in Lemma 4. Note that Point (a) in the definition 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 vrhR on roles for an rh ∗ RBox R such that r vrh R s if, and only if, r v s ∈ R. Let vR be the reflexive, transitive closure of vrh R . Example 5. We illustrates the algorithm in Figure 2 by computing an answer to the question ‘Does C1 = {T , ∅} Σ-entail C2 = {T , R}?’, 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 ∈ N0 determined by the concept name Toe. We have qToe = (Q0 , Q1 , Q2 , Q3 , Q4 ), where Q0 = {Toe}, Q1 = {Toe, ∃isPartOf.Foot}, Q2 = Q1 , Q3 = {(isPartOf, Foot), (isPartOf, ∃isPartOf.Leg)}, Q4 = Q2 . In Step 2, the algorithm checks whether Q2 \ 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 = {(hasLocation, qToe )}. The algorithm computes the quintuple qD determined by the concept D: l l l  D= A u ∃r.( D) . A∈F0 (r,(Q0 ,Q1 ,Q2 ,Q3 ,Q4 ))∈Q D∈Q1 Input: CBoxes C1 = (T1 , R1 ) and C2 = (T2 , R2 ) and signature Σ ⊆ sig(C2 ). 1. Compute the set N0 of quintuples determined by conjunctions of concept names from Σ. 2. If N0 contains a quintuple (Q0 , Q1 , Q2 , Q3 , Q4 ) such that Q2 \ Q4 6= ∅, then output ‘C1 6vΣ C2 ’. 3. Generate the sequence N1 , N2 , ... of sets of quintuples such that Ni+1 = Ni ∪ Ni0 , where Ni0 is the set of quintuples (F0 , F1 , F2 , F3 , F4 ) which can be obtained from a set F0 of concept names from Σ and a set Q ⊆ (Σ ∩ NR ) × Ni of cardinality not exceeding |T2 | in the following way: l l l  – F1 = KC1 A u ∃r.( D) ; A∈F0 (r,(Q0 ,Q1 ,Q2 ,Q3 ,Q4 ))∈Q D∈Q1 l l l  – F2 = KC2 A u ∃r.( D) ; A∈F0 (r,(Q0 ,Q1 ,Q2 ,Q3 ,Q4 ))∈Q D∈Q2  – F3 = (r, D) ∈ (Σ ∩ NR ) × cl(C2 ) | (a) there is a ∃r.C 0 ∈ F1 such that (ID,C2 , D) ≤Σ (IC 0 ,C1 , C 0 ); or (b) there is a (s, (Q0 , Q1 , Q2 , Q3 , Q4 )) ∈ Q such that: ∗ (i) D ∈ Q4 and s vrh R1 r; or rh ∗ ∗ (ii) (t, D) ∈ Q3 , s vR1 r1 , t vrh R1 r2 , and r1 ◦ r2 v r ∈ R1 ;  – F4 = D ∈ cl(C2 ) | (a) for all A ∈ Σ, A ∈ KC2 (D) implies A ∈ F1 ; and (b) for all r ∈ Σ, (D, D0 ) ∈ rID,C2 implies (r, D0 ) ∈ F3 . This is done until Ni contains a quintuple (Q0 , Q1 , Q2 , Q3 , Q4 ) such that Q2 \Q4 6= ∅, or Ni+1 = Ni . Output ‘C1 6vΣ C2 ’ if the first condition applies; otherwise, output ‘C1 vΣ C2 ’. Fig. 2. Algorithm for deciding Σ-entailment in EL with role inclusions. That is, D = D1 u D2 , where D1 = ∃hasLocation.Toe and D2 = ∃hasLocation. ∃isPartOf.Foot. Then qD = (F0 , F1 , F2 , F3 , F4 ) is computed from F0 and Q, where: F1 = {D, D1 , D2 }, F2 = F1 ∪ {∃hasLocation.Foot, ∃hasLocation.Leg}, F3 = {(hasLocation, Toe), (hasLocation, ∃isPartOf.Foot}, F4 = ∅. The algorithm terminates and outputs ‘C1 6vΣ C2 ’ since F2 \ 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 (r, q) ∈ Q, let Figure 2. For each d d Cr,q be the concept which determines the quin- tuple q. Then C = A∈F0 A u (r,q)∈Q ∃r.Cr,q determines (F0 , F1 , F2 , F3 , F4 ). This lemma extends a similar lemma in [11] for EL. Notice that the presence of role inclusions is accounted for by extending the representation of concepts by one additional tuple component. This additional component – the fourth com- ponent of a quintuple – is a set containing pairs of the form (r, D0 ). Intuitively, (r, D0 ) means that the concept represented by the quintuple together with the CBox C1 enforce a role path, which can be abbreviated to r by the RBox, leading to point satisfying a concept, say, C 0 such that C 0 ⇒1 D0 . Finally, we show correctness and complexity of the algorithm in Figure 2. The proof is similar to the one for the corresponding theorem in [11]. Theorem 2 (Correctness and Complexity). The algorithm for deciding Σ- entailment for EL with role inclusions is sound, complete, and runs in exponen- tial time. Proof. Soundness follows from Lemmas 4 and 6. For completeness, assume C v D ∈ Diff Σ (C1 , C2 ). By Lemma 4, C is of outdegree bounded by |C2 | and D ∈ sub(T2 ) such that C2 |= 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 C 0 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 con- cept 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 25|C2 | . Consequently, the algorithm terminates since Nj = Nj+1 , for some j ≤ 25|C2 | . 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 |Q| ≤ |C2 |, is exponential in |C2 |. Moreover, given a pair (F0 , Q), computing the quintuple (F0 , F1 , F2 , F3 , F4 ) in Figure 2 only takes polynomial time in |C2 |. t u 7 Conclusion We have shown that deciding Σ-entailment in EL 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 [8, 16]. The decision procedure is an extension of the algorithm deciding conservative extensions in EL [11]. Thus adding such role inclusion axioms does not increase the complexity of the logical difference problem for EL. For future work, it is interesting to extend the presented algorithmic frame- work to capture more expressivity by, e.g., allowing for more role inclusions, inverse roles, universal roles, nominals, etc. References 1. F. Baader, S. Brandt, and C. Lutz. Pushing the EL envelope. In Proceedings of IJCAI’05, pages 364–369. Professional Book Center, 2005. 2. F. Baader, S. Brandt, and C. Lutz. Pushing the EL envelope further. In Proceedings of OWLED’08: Workshop on OWL – Experiences and Directions, 2008. 3. E. Clarke and H. Schlingloff. Model checking. In Handbook of Automated Reason- ing, volume II, chapter 24, pages 1635–1790. Elsevier Science, 2001. 4. A. Flögel, H. K. Büning, and T. Lettmann. On the restricted equivalence of sub- classes of propositional logic. ITA, 27(4):327–340, 1993. 5. S. Ghilardi, C. Lutz, and F. Wolter. Did I damage my ontology? a case for con- servative extensions in description logics. In Proceedings of KR’06, pages 187–197. AAAI Press, 2006. 6. B. C. Grau, B. Parsia, E. Sirin, and A. Kalyanpur. Modularity and web ontologies. In Proceedings of KR’06, pages 198–209. AAAI Press, 2006. 7. I. Horrocks. Optimising Tableaux Decision Procedures for Description Logics. PhD thesis, University of Manchester, 1997. 8. I. Horrocks, P. F. Patel-Schneider, and F. van Harmelen. From SHIQ and RDF to OWL: The Making of a Web Ontology Language. Journal of Web Semantics, 1(1):7–26, 2003. 9. B. Konev, D. Walther, and F. Wolter. The logical difference problem for description logic terminologies. In Proceedings of IJCAR’08. Springer-Verlag, 2008. To appear. 10. C. Lutz, D. Walther, and F. Wolter. Conservative extensions in expressive descrip- tion logics. In Proceedings of IJCAI’07, pages 453–458. AAAI Press, 2007. 11. C. Lutz and F. Wolter. Conservative extensions in the lightweight description logic EL. In Proceedings of CADE’07. Springer, 2007. 12. N. F. Noy and M. Musen. Promptdiff: A fixed-point algorithm for comparing ontology versions. In Proceedings of AAAI, pages 744–750, 2002. 13. D. Pokrywczynski and D. Walther. Deciding the logical difference problem for EL with role inclusions. manuscript, http://www.csc.liv.ac.uk/~dirk/. 14. A. L. Rector and I. Horrocks. Experience building a large, re-usable medical on- tology using a description logic with transitivity and concept inclusions. In Pro- ceedings of the Workshop on Ontological Engineering, AAAI Spring Symposium, pages 100–107. Hanley and Belfus, 1997. 15. N. Sioutos, S. de Coronado, M. W. Haber, F. W. Hartel, W.-L. Shaiu, and L. W. Wright. NCI Thesaurus: A semantic model integrating cancer-related clinical and molecular information. Journal of Biomedical Informatics, 40(1):30–43, 2007. 16. K. A. Spackman. Managing clinical terminology hierarchies using algorithmic cal- culation of subsumption: Experience with SNOMED-RT. Journal of the American Medical Informatics Association, Fall Symposium Special Issue, 2000. 17. The Gene Ontology Consortium. Gene ontology: tool for the unification of biology. In Nature Genetics, volume 25, 2000. 18. S. Tobies. Complexity Results and Practical Algorithms for Logics in Knowledge Representation. PhD thesis, RWTH Aachen, 2001.