Ontologies are used to represent and share knowledge. Numerous ontologies have been developed so far, especially in knowledge intensive areas such as the biomedical domain. As the size of ontologies increases, their continued development and maintenance is becoming more challenging as well. Detecting and representing semantic di erences between versions of ontologies is an important task for which automated tool support is needed. In this paper we investigate the logical di erence problem using a hypergraph representation of EL-terminologies. We focus solely on the concept di erence wrt. a signature. For computing this di erence it su ces to check the existence of simulations between hypergraphs whereas previous approaches required a combination of di erent methods.
We thank the reviewers of the workshop DChanges 2013 for their comments. The authors acknowledge the support of the German Research Foundation (DFG), Andreas Ecke within GRK 1763 (QuantLA), and Michel Ludwig and Dirk Walther within the Resilience and Bio Path of the Cluster of Excellence `Center for Advancing Electronics Dresden'. 1http://www.w3.org/TR/owl2-overview/ 2http://bioportal.bioontology.org This work is licensed under the Creative Commons AttributionShareAlike 3.0 Unported License (CC BY-SA 3.0). To view a copy of the license, visit http://creativecommons.org/licenses/by-sa/3.0/. comes more challenging as well. For instance, the ontology SNOMED CT contains now de nitions for about 400 000 terms, and the `NCBI organismal classi cation' ontology even for about 850 000 terms. In particular, the need to have automated tool support for detecting and representing di erences between versions of an ontology is growing in importance for ontology engineering. Current support from ontology editors, such as Protege, SWOOP, OBO-Edit, and OntoView, is mostly based on syntactic di erences and does not capture the semantic di erences between ontologies. An early detection of possibly unwanted semantic changes can contribute to an error-resilient authoring process of ontologies.
The aim of this paper is to propose and investigate the
logical di erence problem using a hypergraph
representation of ontologies. The logical di erence problem was
introduced in [
An EL-terminology can easily be translated into a directed hypergraph by taking the signature symbols as nodes and treating the axioms as hyperedges. For instance, the axiom A v 9r:B is translated into the hyperedge (fxAg; fxr; xBg), and the axiom A B1 u B2 into the three hyperedges (fxAg; fxB1 g), (fxAg; fxB2 g) and (fxB1 ; xB2 g; fxAg), where each node xY corresponds to the signature symbol Y , respectively. A feature of the translation of axioms into hyperedges is that all information about the axiom and the logical operators in it is preserved. We can actually treat the ontology and its hypergraph interchangeably. The existence of certain simulations between hypergraphs characterises the fact that the corresponding terminologies are logically equivalent and, thus, no logical di erence exists. If no simulation exists, we can directly extract the axioms responsible for the concept inclusion that witnesses the logical di erence from the hypergraph.
The main advantages of the hypergraph-based approach to
logical di erence are: (i) an elegant algorithm for detecting
the existence of concept di erences (solely involving
checking for simulations in hypergraphs), even for large or cyclic
terminologies; (ii) a straightforward way to construct
concept inclusions that witness the logical di erence between
two terminologies, even for cyclic terminologies; and (iii) a
simple computation of explanations, i.e., sets of axioms that
entail such concept inclusions. Currently, the algorithms
implemented for detecting the logical di erence work for large
but acyclic terminologies such as SNOMED CT [5{7]. The
algorithm in [
The paper is organised as follows. We start by reviewing
some notions regarding the description logic EL, the logical
di erence problem, and ontology hypergraphs. In Section 3,
we introduce two simulation notions, a forward and a
backward simulation, one for each type of concept inclusion that
may witness the logical di erence between two
terminologies. In each case we show that the existence of a
simulation between two terminologies corresponds to the absence
of di erence witnesses. We analyse the computational
complexity of checking for simulations, and we sketch how to
construct counter-examples. In Section 4, we discuss
previous approaches to computing the logical di erence in [
We start by brie y reviewing the lightweight description logic EL and some notions related to the logical di erence, together with some basic results. 2.1 The Logic EL Let NC and NR be mutually disjoint sets of concept names and role names. We assume these sets to be countably in nite. We typically use A; B to denote concept names and r to denote role names. The set of EL-concepts C is de ned inductively as: > and all concept names in NC are EL-concepts, if C; D are EL-concepts, then C u D and 9r:C are ELconcepts, where r 2 NR.
An EL-TBox T is a nite set of axioms, where an axiom can be a concept inclusion C v D, or a concept equation C D, where C; D range over EL-concepts.
The semantics of EL is de ned using interpretations I =
( I ; I ), where the domain I is a non-empty set, and I is a
function mapping each concept name A to a subset AI of I
and every role name r to a binary relation rI over I . The
extension CI of a concept C is de ned inductively as follows:
>I := I , (C u D)I := CI \ DI and (9r:C)I := fx 2 I j
9y 2 CI : (x; y) 2 rI g. An interpretation I satis es a
concept C, an axiom C v D or C D if, respectively,
CI 6= ;, CI DI , or CI = DI . We write I j= if I
satis es the axiom . An interpretation I satis es a TBox T
if I satis es all axioms in T ; in this case, we say that I is
a model of T . An axiom follows from a TBox T , written
T j= , if for all models I of T , we have that I j= .
Checking that T j= can be done in polynomial time in the
size of T and [
A signature is a nite set of symbols from NC and NR. The signature sig(C), sig( ) or sig(T ) of the concept C, axiom or TBox T is the set of concept and role names occurring in C, or T , respectively. An EL -concept C is an EL-concept such that sig(C) .
Two TBoxes T and T 0 are logically equivalent wrt. a
signature , written T T 0, if for all EL-axioms with
sig( ) : T j= i T 0 j= . In other words, two TBoxes
are logically equivalent wrt. a signature if the same axioms
formulated in the signature follow from them. In this case,
the TBoxes are also said to be -inseparable.
Conservative extensions are a special case of logical equivalence: for
T T 0 and = sig(T ), T 0 is a conservative extension of
T wrt. i T T 0. Deciding the logical equivalence of
EL-TBoxes wrt. a signature is ExpTime-complete [
Lemma 1. For every EL-TBox T , there is a attened ELTBox T ' of polynomial size in the size of T such that T T 0 with = sig(T ).
For the remainder of the paper we assume that TBoxes are attened.
An important motivating feature of EL is that it exhibits
a low complexity for standard reasoning tasks. However,
as we have seen above, deciding the logical equivalence of
EL-TBoxes wrt. a signature already requires exponential
time.3 To gain tractability for deciding the logical
equivalence, TBoxes are restricted to a particular form as in [
De nition 1. An EL-TBox T is called an EL-terminology
if it satis es the following conditions:
3Note that it is tractable to check the logical equivalence of
two EL-TBoxes without restricting the signature [
The restriction to EL-terminologies yields that deciding
logical equivalence wrt. a signature becomes tractable [
In this paper we do not restrict terminologies to be acyclic.
However, we have to take care of certain cycles. In our
approach we want all conjunctions to be unfolded. That is,
for any conjunction A1 u u Am in T , we substitute any
Ai with B1 u u Bn if Ai B1 u u Bn 2 T . To this end
we need to handle the cycles along such concept equations.
Formally, a terminology T has unfoldable conjunctions if it
does not contain any concept equations A1 F1; : : : ; An
Fn, where F1; : : : ; Fn are conjunctions of concept names such
that Ai+1 2 sig(Fi) for every 1 i < n, and A1 2 sig(Fn).
Any terminology can be rewritten such that it has unfoldable
conjunctions without changing the logical consequences (cf.
proof of Lemma 1 in [
To simplify the presentation we assume that terminologies do not contain trivial axioms of the form A > or A B, where A and B are concept names.
An EL-terminology T is normalised if it consists of ELconcept inclusions and equations of the following forms: A 9r:B, A 9r:>, A
B1 u : : : u Bm, and
A v 9r:B, A v 9r:>, A v B1 u : : : u Bn, where m 2, n 1, and A, B, Bi are concept names such that every conjunct Bi is non-conjunctive in T .
The logical di erence between two TBoxes witnessed by concept inclusions over a signature is de ned as follows.
De nition 2. The -concept di erence between two ELTBoxes T1 and T2 for a signature is the set Di (T1; T2) of all EL-concept inclusions such that sig( ) , T1 j= , and T2 6j= .
As the set Di (T1; T2) is in nite in general, we make use
of the following \primitive witnesses" theorem from [
Theorem 1 (Primitive witnesses). Let T1 and T2 be EL-terminologies and a signature. If 2 Di (T1; T2), then either C v A or A v D is a member of Di (T1; T2), where A 2 sig( ) is a concept name and C, D are ELconcepts occurring in .
We de ne cWtnlhs(T1; T2) as the set of all concept names A from such that there exists an EL -concept C with A v C 2 Di (T1; T2). Similarly, cWtnrhs(T1; T2) is the set of all concept names A 2 such that there exists an EL concept C with C v A 2 Di (T1; T2). The concept names in cWtnlhs(T1; T2) are called left-hand side witnesses and the concept names in cWtnrhs(T1; T2) right-hand side witnesses. Note that these sets are subsets of , and by Theorem 1 their union is a nite and succinct representation of the set Di (T1; T2), which is typically in nite.
Checking for the concept di erence between two terminologies equals checking for the existence of left- and right-hand side witnesses. As a corollary of Theorem 1, we have that: Di (T1;T2) = ;i cWtnlhs(T1;T2) = ; and cWtnrhs(T1;T2) = ;.
Hypergraphs are a generalisation of graphs with many
applications in computer science and discrete mathematics.
In knowledge representation hypergraphs have been used
implicitly to de ne reachability-based modules of
ontologies [
De nition 3. For a normalised terminology T and a signature , the ontology hypergraph GT of T for is a directed hypergraph GT = (V; E) de ned as follows: V = f xA j A 2 NC \ ( [ sig(T )) g
[ f xr j r 2 NR \ ( [ sig(T )) g and
[ fx>g E = f (fxAg; fxBi g) j A v B1 u : : : u Bn 2 T ; 1 [ f (fxAg; fxBi g) j A
B1 u : : : u Bn v T ; 1 [ f (fxAg; fxr; xY g) j A v 9r:Y 2 T ; Y 2 NC [ f>g g [ f (fxAg; fxr; xY g) j A [ f (fxr; xY g; fxAg) j A 9r:Y 2 T ; Y 2 NC [ f>g g 9r:Y 2 T ; Y 2 NC [ f>g g [ f (fxB1 ; : : : ; xBn g; fxAg) j A B1 u : : : u Bn 2 T g i i n g n g An ontology hypergraph GT contains a node for > and for every role and concept name in or T . Hyperedges in GT represent axioms in T . Every hyperedge is directed and can be understood as an implication, i.e., (fxAg; fxBg) represents T j= A v B. The complex hyperedges are of the form (fxAg; fxr; xBg) and (fxr; xBg; fxAg) representing T j= A v 9r:B and T j= 9r:B v A, and of the form (fxB1 ; :::; xBn g; fxAg) standing for T j= B1 u : : : u Bn v A. Note that due to the normalisation of T , conjunctions always have more than one conjunct (i.e. n 2).
Example 1. Let T = fA B1uB2uB3; B3 v 9r:B4; B4 v B1g and = fB5g. Then the ontology hypergraph GT of T for can be depicted as follows: xB5
x> xB4
Our approach for detecting logical di erences wrt. is based
on nding appropriate simulations between the hypergraphs
GT1 and GT2 such that every node xA in GT1 with A 2 is
simulated by the node xA in GT2 . It is well known that the
existence of a simulation between two graph structures can
be used to characterise some notion of equivalence between
the graphs [
We rst introduce an auxiliary relation !T over the nodes
of the ontology hypergraph GT of the terminology T . The
relation !T is a special reachability notion in GT that
mimics reasoning wrt. T . The de nition of !T is related to
the completion algorithm for classi cation in EL [
De nition 4. Let GT = (V; E) be the ontology hypergraph of a normalised terminology T for a signature . The relation !T V(1) V(2) is inductively de ned as follows, where V(k) = f S V j 0 < jSj k g: (i) fxg !T fxg for every x 2 V; (ii) fxg !T fzg if fxg !T fyg, (fyg; fzg) 2 E; (iii) fxg !T fxr; zg if fxg !T fyg, (fyg; fxr; zg) 2 E; (iv) fxg !T fzg if fxg !T fxr; yg, fyg !T fy0g, and (fxr; y0g; fzg) 2 E; (v) fxg !T fzg if fxg !T fxr; yg, (fxr; x>g; fzg) 2 E; (vi) fxg !T fzg if fxg !T fyig for all i 2 f1; : : : ; ng, (fy1; : : : ; yng; fzg) 2 E.
Note that the relation !T associates nodes xA that represent concept names A either with nodes xB that stand for concept names B or with pairs of nodes fxr; zg representing concepts of the form 9r:A or 9r:>. The binary relation !T is re exive and transitive on single nodes by Conditions (i) and (ii). Moreover, in Condition (vi) transitivity of !T is extended to hyperedges with complex left-hand sides, representing axioms of the form A B1 u: : :uBn. The other conditions handle pairs of nodes. Condition (iii) states that any indirectly reachable pair fxr; zg via an intermediate node is also directly reachable via !T , while Condition (iv) ensures the same property for indirectly reachable nodes via intermediate pairs. Condition (v) is a special case of (iv) for handling pairs involving > as ontology hypergraphs for normalised terminologies T do not contain hyperedges from nodes xA representing concept names to x> representing > (T does not contain any axioms of the form A v > or A >).
It can be readily seen that the relation !T can be computed in polynomial time.
We emphasise here that the relation !T does not coincide with the usual reachability notion in a hypergraph. The following example shows that !T connects reachable nodes but not all reachable nodes are connected via !T . This means that the usual reachability relation does not correctly mimic logical consequences entailed by T .
Example 2. Let T = fA v 9r:B0; 9r:B0 v B; 9r:B v A0g. It holds that fxAg !T fxBg, i.e. T j= A v B, and the node xB is reachable from xA (in terms of standard graph reachability). However, xA0 is also reachable from xA whereas fxAg 6!T fxA0 g and T 6j= A v A0.
The notion of reachability induced by the relation !T can be characterised in terms of entailment.
Lemma 2. Let GT = (V; E) be the ontology hypergraph of a normalised terminology T for a signature . Then we have for every A; B; r 2 [ sig(T ): (i) T j= A v B i fxAg !T fxBg; (ii) T j= A v 9r:B i fxAg !T fxr; xB0 g and fxB0 g !T fxBg for some B0 2 [ sig(T ); (iii) T j= A v 9r:> i fxAg !T fxr; xY g for some Y 2 [ sig(T ) [ f>g.
GT1 and GT2 . subsections.
As described above, we want to check for every concept name A 2 whether A belongs to cWtnlhs(T1; T2) or to cWtnrhs(T1; T2). For the former, we check for the existence of a forward simulation, and for the latter, for the existence of a backward simulation between the ontology hypergraphs We de ne the simulations in the following
Based on the relation !T we can now give the de nition of the forward simulation, which connects nodes in GT1 with nodes in GT2 that are reachable via !T1 and !T2 , respectively.
De nition 5. Let GT1 = (V1; E1), GT2 = (V2; E2) be ontology hypergraphs of two normalised terminologies T1 and T2 for a signature . A relation ,!f V1 V2 is a forward simulation between GT1 and GT2 if the following conditions hold: (if ) if xA , f xA0 , then for every B 2
! fxBg it holds that fxA0 g !T2 fxBg; (iif ) if xA ,!f xA0 , then for every r 2 such that fxAg !T1 fxr; xX g there is a xX0 2 V2 such that fxA0 g !T2 fxr; xX0 g and xX ,!f xX0 .
We write GT1 ,!f GT2 i there exists a forward -simulation ,!f V1 V2 such that (xA; xA) 2 ,!f for every A 2 . For a node xA in GT1 to be forward simulated by xA0 in GT2 , Condition (if ) enforces that every -concept name B that is entailed by A in T1 must also be entailed by A0 in T2. Condition (iif ) ensures a similar requirement for concepts of the form 9r:X with X 2 sig(T1) [ f>g such that T1 j= A v 9r:X while propagating the simulation to the successor node xX .
Example 3. Let T1 = fA v 9r:Ag, T2 = fA v 9r:X; X v A u Y; Y v 9r:Xg, and = fA; rg. Then one can see that Di (T1; T2) = ;. Furthermore, wrt. GT1 it only holds that fxAg !T1 fxAg, fxAg !T1 fxr; xAg. Regarding GT2 , we have fxAg !T2 fxAg, fxAg !T2 fxr; xX g, fxX g !T2 fxAg, fxX g !T2 fxr; xX g. Hence, one can see that S = f(xA; xA); (xA; xX )g is a forward -simulation between GT1 and GT2 with (xA; xA) 2 S. A graphical representation of the ontology hypergraphs GT1 , GT2 and of the simulation S can be found below.
GT2 xA x>
Example 4. Let T1 = fA v 9r:X; X v AuBg, T2 = fA v X u Y; X v 9r:A; Y v 9r:Bg, and = fA; B; rg. Then, for instance, A v 9r:(A u B) 2 Di (T1; T2). It holds that fxAg !T1 fxr; xX g, fxX g !T1 fxAg, fxX g !T1 fxBg, fxAg !T2 fxr; xAg, fxAg !T2 fxr; xBg. However, for x = xA or x = xB it does not hold that fxg !T2 fxAg and fxg !T2 fxBg, i.e. the node xX in GT1 cannot be simulated by xA or xB in GT2 as Condition (if ) cannot be satis ed. Thus, one can see that there cannot exist a forward -simulation S between GT1 and GT2 with (xA; xA) 2 S. with fxAg !T1
GT1 ,!f GT2 .
We now prove that the existence of a forward simulation between a node xA1 in GT1 and a node xA2 in GT2 exactly captures the property that T1 j= A1 v C entails that T2 j= A2 v C for every -concept C.
Lemma 3. Let T1; T2 be normalised terminologies, and let be a signature such that GT1 ,!f GT2 . Then for every EL -concept C and for every (xA1 ; xA2 ) 2 ,!f with T1 j= A1 v C it holds that T2 j= A2 v C. let
Lemma 4. Let T1; T2 be normalised terminologies, and be a signature such that cWtnlhs(T1; T2) = ;. Then We obtain Theorem 2 as a consequence of the previous two lemmas. let GT2 .
Theorem 2. Let T1; T2 be normalised terminologies, and be a signature. Then cWtnlhs(T1; T2) = ; i GT1 ,!f
We now turn to right-hand side witnesses, i.e. we want to devise an algorithm that checks whether cWtnrhs(T1; T2) = ;. Analogously as for the left-hand side witnesses, we introduce a backward simulation which has the property that a node xA1 in GT1 is simulated by a node xA2 in GT2 i T1 j= C v A1 entails T2 j= C v A2 for every -concept C. Intuitively, the hypergraph has to be traversed backwards to identify all essential concepts C for which T1 j= C v A1. In particular, concept names A1 for which there does not exist an EL concept C with T1 j= C v A1 do not have to be simulated by a node in GT2 since such concept names cannot become righthand side witnesses. We identify such concept names A1 by checking whether the node xA1 is -entailed in the following sense.
De nition 6. Let GT = (V; E) be the ontology hypergraph of a normalised terminology T for a signature . Moreover, let V V be the smallest set of nodes de ned inductively as follows: (i) x> 2 V ; (ii) if xA 2 V such that there exists B 2 fxAg, then xA 2 V ; with fxBg !T (iii) if xB 2 V with B 2 NC [ f>g, (fxB; xrg; fxAg) 2 E, and r 2 , then xA 2 V ; (iv) if xB1 ; : : : ; xBn 2 V then xA 2 V .
with (fxB1 ; : : : ; xBn g; fxAg) 2 E, We then say that a node x 2 V is -entailed in GT i x 2 V . The node x> is always -entailed for every signature . A node x is -entailed if it is reachable via !T from a node xB with B 2 , or if its direct predecessors in the ontology hypergraph are -entailed. In particular, every node xA with A 2 is -entailed.
Example 5. Let T = fA 9r:X; X B1uB2g. For 1 = fB1; B2; rg, all the nodes are 1-entailed in GT 1 . However, for 2 = fB1; B2g only the nodes xB1 , xB2 xX , and x> are 2-entailed in GT 2 , whereas for 3 = fB1; rg only the node x> is 3-entailed in GT 3 . Note that T j= C v A holds for C = 9r:(B1 u B2) and sig(C) 1 but sig(C) 6 2 and sig(C) 6 3.
Lemma 5. Let GT = (V; E) be the ontology hypergraph of a normalised terminology T for a signature , and let xA 2 V. Then the node xA is -entailed in GT i there exists an EL -concept C such that T j= C v A. To compute all the nodes in a given graph GT that are entailed, we can proceed as follows. In a rst step identify all the nodes x that ful ll conditions (i) and (ii) by using the relation !T . Subsequently, propagate the -entailed status to other nodes using conditions (iii) and (iv). It can be readily seen that these computation steps can be performed in polynomial time.
Before we can give the de nition of the backward
simulation, we have to introduce the following notion: we associate
with every node xA in a hypergraph GT a set of concept
names non-conj(xA) which are \essential" to entail A in T
(also see [
De nition 7. Let GT = (V; E) be an ontology hypergraph. For xA 2 V, let non-conj(xA) be de ned as follows if (fxB1 ; : : : ; xBn g; fxAg) 2 E, let otherwise, let non-conjT (xA) = fxAg:
non-conjT (xA) = fxB1 ; : : : ; xBn g; For a graph GT = (V; E) we have (fxB1 ; : : : ; xBn g; fxAg) 2 E i A B1 u : : : u Bn 2 T . Hence, it holds for every EL concept C that T j= C v A i T j= C v X for every X 2 f X j xX 2 non-conjT (xA) g.
We can now give the de nition of a backward simulation.
De nition 8. Let GT1 = (V1; E1), GT2 = (V2; E2) be the ontology hypergraphs of the normalised terminologies T1 and T2 for a signature . A relation ,!b V1 V2 is a backward -simulation between GT1 and GT2 if the following conditions hold:
such that xX ,!b xXi0 ; (ib) if xA , b xA0 , then for every B 2
! fxAg it holds that fxBg !T2 fx0Ag; with fxBg !T1 (iib) if xA ,!b xA0 and (fxX ; xrg; fxAg) 2 E1 such that r 2 and xX is -entailed in GT1 , then for every xBi0 2 non-conjT2 (xA0 ) there exists (fxXi0 ; xrg; fxBi0 g) 2 E2 (iiib) if xA ,!b xA0 and (fxB1 ; : : : xBn g; fxAg) 2 E1 where xBi are -entailed in GT1 for every 1 i n, then for every x0 2 non-conjT2 (xA) there exists an x 2 non-conjT1 (xA) with x ,!b x0.
In the following, we write GT1 ,!b GT2 i there exists a backward -simulation ,!b V1 V2 with (xA; xA) 2 ,!b for every A 2 .
For a node xA in GT1 to be backward simulated by xA0 in GT2 , Conditions (ib) and (iib) are the equivalent of the Conditions (if ) and (iif ), respectively, for forward simulations. Condition (iiib) handles axioms of the form A B1 u: : :uBn in T1. Note that we quantify over the conjuncts of A0 in T2 since, intuitively speaking, fewer conjuncts su ce to preserve logical entailments. Take, for instance, the two normalised terminologies T1 = fA B1 u B2g, T2 = fA v B1 u B2; B1 v Ag and the signature = fA; B1; B2g; then cWtnrhs(T1; T2) = ; and, in particular, T2 j= B1 u B2 v A holds as well.
Example 6. Let T1 = fA 9r:X; X B1 u B2g, T2 = fA XuY; X 9r:B1; Y 9r:B2g, and = fA; B1; B2; rg. First we observe that the nodes xB1 , xB2 , xX , and xA are -entailed in GT1 . As only fxBi g !T1 fxBi g for i 2 f1; 2g, one can see that the node xBi in GT1 can be simulated by the node xBi in GT2 for i 2 f1; 2g. Due to non-conjT2 (xBi ) = fxBi g for i 2 f1; 2g and non-conjT1 (xX ) = fxB1 ; xB2 g, we can infer that the node xX in GT1 can be simulated both by xB1 and xB2 in GT2 (there does not exist X0 2 with fxX0 g !T1 fxX g). Finally, as non-conjT2 (xA) = fxX ; xY g, we conclude that the node xA in GT1 can be simulated by xA in GT2 due to Condition (iib) (Condition (ib) is trivially satis ed). Overall, S = f(xA; xA); (xX ; xB1 ); (xX ; xB2 ); (xB1 ; xB1 ); (xB2 ; xB2 )g is a backward -simulation between GT1 and GT2 such that (Z; Z) 2 S for every Z 2 NC \ . A graphical representation of the ontology hypergraphs GT1 , GT2 and of the simulation S can be found below.
GT1 x> xr xA xB1 xX xB2
xA xY
xX xB2 xr
GT2 xB1 x>
Example 7. Let T1 = fA B1 u B2g, T2 = fA B1 u B0g, and = fA; B1; B2g. First we observe that there does not exist a concept name Z 2 with fxZ g !T2 fxB0 g, i.e. the nodes xB1 , xB2 in GT1 cannot be simulated by xB0 in GT2 as Condition (ib) would be violated. Hence, as non-conjT1 (xA) = fxB1 ; xB2 g and as non-conjT2 (xA) = fxB1 ; xB0 g, we can conclude that there cannot exist a backward -simulation such that xA in GT1 is simulated by xA in GT2 as Condition (iiib) cannot be ful lled.
We can now establish the correctness and completeness properties regarding backward simulations.
Lemma 6. Let T1; T2 be normalised terminologies, and let be a signature such that GT1 ,!b GT2 . Then for every EL -concept C and for every (xA1 ; xA2 ) 2 ,!b with T1 j= C v A1 it holds that T2 j= C v A2.
Lemma 7. Let T1; T2 be normalised terminologies, and let be a signature such that cWtnrhs(T1; T2) = ;. Then GT1 ,!b GT2 .
We obtain Theorem 3 as a consequence of the previous two lemmas.
Theorem 3. Let T1; T2 be normalised terminologies, and let be a signature with A 2 . Then cWtnrhs(T1; T2) = ; i GT1 ,!b GT2 . 3.3
Given two hypergraphs GT1 = (V1; E1) and GT2 = (V2; E2), ohnoledsc.anFpirrsotc,eleedt aSs0f folloVw1s toV2chbeeckthwehesethteorf GaTll1 t,!hefpaGiTr2s that ful ll Conditions (if ). Subsequently, iterate over the elements contained in the set Sif and remove those pairs which do not satisfy Conditions (iif ) to obtain the set Sif+1. Eventually we will have Sjf = Sj+1 for some index j and one f can conclude that GT1 ,!f GT2 holds i (xA; xA) 2 Sjf for every A 2 .
It is easy to see that the simulation Conditions (if ) and (iif ) can be checked in polynomial time. Thus, as the procedure described above terminates in at most jV1 V2j iterations, we can infer that it can be checked in polynomial time whether GT1 ,!f GT2 holds.
Similar arguments show that the existence of a backward simulation can be checked in polynomial time as well, which gives us the following result.
Theorem 4. Let GT1 = (V1; E1), GT2 = (V2; E2) be ontology hypergraphs of two normalised terminologies T1 and T2 for a signature . Then it can be checked in polynomial time whether GT1 ,!f GT2 and GT1 ,!b GT2 holds.
Note that in a practical implementation it would not be required to take the complete ontology graphs GT1 and GT2 into account if one wants to check whether a concept name A 2 is a di erence witness. It is su cient to consider the subgraph only which is induced by the !T1 and !T2 either in the \forward" or \backward" direction depending on the type of witnesses that should be computed. For a typical (practical) terminology T , S !T S0 only holds for relatively few sets of nodes S; S0, which suggests that the number of nodes that have to be considered for a simulation check should remain fairly small as well.
So far we have focused on nding di erence witnesses, i.e. concept names A belonging either to the set cWtnlhs(T1; T2) or the set cWtnrhs(T1; T2), which is su cient to decide the existence of a logical di erence between T1 and T2. However, in practical applications of logical di erence it can be helpful for users to have a concrete concept inclusion C v A or A v D in Di (T1; T2) that corresponds to a witness A. We now sketch how to read such concept inclusions directly o a hypergraph using Example 7.
Recall that xB1 , xB2 in GT1 cannot be simulated by xB0 in GT2 as T2 6j= B1 v B0 and T2 6j= B2 v B0, i.e. for the -concept C = B1 u B2 it holds that T1 j= C v B1 u B2, but T2 6j= C v B1 u B0. Hence, we have T1 j= C v A but T2 6j= C v A.
In general, if a node xA in GT1 cannot be simulated by xA
in GT2 , there exists a node x in GT2 which is the main cause
for the failure to nd a simulation (x = xB0 in the example
above). By following the path from that node to the node xA
in GT2 and by constructing conjunctions over all the failing
possibilities to ful ll the simulation conditions (B1 u B2 in
the example above) one can construct an example inclusion
C v A (or A v C) that matches the di erence witness A.
The correctness of the algorithm described above can be seen
by using Lemma 2. It is known that such concepts C can be
of exponential size [
We now compare the hypergraph-based approach with the
previous method for detecting logical di erences that is
developed in [
Fundamental di erences can be found regarding the
computation of right-hand side witnesses. Recall from Section 2.3
that A 2 cWtnrhs(T1; T2) i there exists a -concept C such
that T1 j= C v A but T2 6j= C v A. The general aim of [
Two di erent algorithms are then presented in [
Algorithm 2 uses a dynamic programming approach to
derive conditions that allow us to identify which concepts in
noimplyTn2; (A) are relevant for deciding whether A is a
righthand side witness. This approach has been implemented in
the logical di erence tool CEX [
We have presented a novel approach to the logical di erence
problem using a hypergraph representation of ontologies. As
ontologies we consider (possibly cyclic) terminologies given
in the description logic EL. As di erences between
terminologies we only consider EL-concept inclusions formulated
in a given signature. A terminology is transformed into a
hypergraph by taking the signature symbols as nodes and
treating the axioms as hyperedges. We have devised two
simulation notions between hypergraphs. The existence of
the simulations is equivalent to the fact that every concept
inclusion which is formulated in the considered signature
and which follows from the rst corresponding terminology
also follows from the second terminology. Checking for the
existence of simulations is tractable, con rming the
established complexity bounds in [