In this paper we are concerned with the logical difference problem between ontologies. The logical difference is the set of subsumption queries that follow from a first ontology but not from a second one. We revisit our solution to logical difference problem for EL-terminologies based on finding simulations between hypergraph representations of the terminologies, and we investigate a possible extension of the method to general EL-TBoxes.
Ontologies are widely used to represent domain knowledge. They contain
specifications of objects, concepts and relationships that are often formalised using
a logic-based language over a vocabulary that is particular to an application
domain. Ontology languages based on description logics [
Ontologies constantly evolve, they are regularly extended, corrected and refined. As the size of ontologies increases, their continued development and maintenance becomes more challenging as well. In particular, the need to have automated tool support for detecting and representing differences between versions of an ontology is growing in importance for ontology engineering.
The logical difference is taken to be the set of queries that produce
different answers when evaluated over distinct versions of an ontology. The language
and vocabulary of the queries can be adapted in such a way that exactly the
differences of interest become visible, which can be independent of the
syntactic representation of the ontologies. We consider ontologies formulated in the
? The second and third authors were supported by the German Research Foundation
(DFG) within the Cluster of Excellence ‘Center for Advancing Electronics Dresden’.
3 http://www.w3.org/TR/owl2-overview/
4 http://bioportal.bioontology.org
lightweight description logic E L [
The logical difference problem was introduced in [
We first show that for every concept inclusion C v D that follows from a
TBox T , there exists a concept name X in T that acts as an interpolant between
the concepts C and D, i.e., we have that T |= C v X and T |= X v D. Then we
describe the set of all subsumees C of X in T using a concept of E L extended
with disjunction and a least fixpoint operator, and the set of all subsumers D of
X in T using a concept of E L extended with greatest fixpoint operators. Finally,
we reduce the problem of deciding the logical difference between two E L-TBoxes
to fixpoint reasoning w.r.t. TBoxes in a hybrid μ-calculus [
The paper is organised as follows. We start by recalling some notions regarding the description logic E L and its extensions with disjunction and fixpoint operators. In Section 3, we discuss how the logical difference problem for E L-terminologies could be extended to general E L-TBoxes, and we establish a witness theorem for general E L-TBoxes. In Section 4, we show how fixpoint reasoning can be used to decide whether two general E L-TBoxes are logically different, and how witnesses to the logical difference can be computed. Finally we conclude the paper. 2
We start by briefly reviewing the lightweight description logic E L and some notions related to the logical difference, together with some basic results.
Let NC, NR, and NV be mutually disjoint sets of concept names, role names, and variable names, respectively. We assume these sets to be countably infinite. We typically use A, B to denote concept names and r to denote role names.
The sets of E L-concepts C, E LU μ-concepts D, and E Lν -concepts E are built according to the following grammar rules:
C ::= > | A | C u C | ∃r.C D ::= > | A | D u D | D t D | ∃r.D | x | μx.D
E ::= > | A | E u E | ∃r.E | x | νx.E 5 http://dl.kr.org/ore2014/ where A ∈ NC, r, s ∈ NR, and x ∈ NV. For an ELU μ-concept C, the set of free variables in C, denoted by FV(C) is defined inductively as follows: FV(>) = ∅, FV(A) = ∅, FV(D1 u D2) = FV(D1) ∪ FV(D2), FV(D1 t D2) = FV(D1) ∪ FV(D2), FV(∃r.D0) = FV(D0), FV(x) = {x}, FV(μx.D0) = FV(D0) \ {x}. The set FV(E) of free variables occurring in an ELν -concept E can be defined analogously. An ELU μ-concept C (an ELν -concept D) is closed if C (D) does not contain free occurrences of variables, i.e. FV(C) = ∅ (FV(D) = ∅). In the following we assume that every ELU μ-concept C and every ELν -concept D is closed.
An EL-TBox T is a finite set of axioms, where an axiom can be a concept inclusion C v C0, or a concept equation C ≡ C0, where C, C0 range over ELconcepts. An EL-terminology T is an EL-TBox consisting of axioms α of the form A v C and A ≡ C, where A is a concept name, C an EL-concept and no concept name A occurs more than once on the left-hand side of an axiom.
The semantics of EL, ELU μ, and ELν is defined 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 ⊆ ΔI ×ΔI . Interpretations are extended to concepts using a function ·I,ξ that is parameterised by an assignment function that maps variables x ∈ NV to sets ξ(x) ⊆ ΔI . Given an assignment ξ, the extension of an EL, ELU μ, or ELν -concept is defined inductively as follows: >I,ξ := ΔI , xI,ξ := ξ(x) for x ∈ NV, (C1 u C2)I,ξ := C1I ∩ C2I , (∃r.C)I,ξ := { x ∈ ΔI | ∃y ∈ CI,ξ : (x, y) ∈ rI }, (μx.C)I,ξ = T{ W ⊆ ΔI | CI,ξ[x7→W ] ⊆ W }, and (νx.C)I,ξ = S{ W ⊆ ΔI | W ⊆ CI,ξ[x7→W ] }, where ξ[x 7→ W ] denotes the assignment ξ modified by mapping x to W .
An interpretation I satisfies a concept C, an axiom C v D or C ≡ D if,
respectively, CI,∅ 6= ∅, CI,∅ ⊆ DI , or CI,∅ = DI,∅. We write I |= α iff I
satisfies the axiom α. An interpretation I satisfies a TBox T iff I satisfies 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 |= α, iff for all models I of T , we have that I |= α.
Deciding whether T |= C v C0, for two EL-concepts C and C0, can be done in
polynomial time in the size of T and C, C0 [
A signature Σ is a finite 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) ⊆ Σ.
An EL-TBox T is normalised if it only contains EL-concept inclusions of the
forms > v B, A1 u . . . u An v B, A v ∃r.B, or ∃r.A v B, where A, Ai, B ∈ NC,
r ∈ NR, and n ≥ 1. Every EL-TBox T can be normalised in polynomial time in
the size of T with a linear increase in the size of the normalised TBox w.r.t. T
such that the resulting TBox is a conservative extension of T [
E L-TBoxes The logical difference between two TBoxes witnessed by concept inclusions over a signature Σ is defined as follows.
Definition 1. The Σ-concept difference between two EL-TBoxes T1 and T2 for a signature Σ is the set cDiffΣ(T1, T2) of all EL-concept inclusions α such that sig(α) ⊆ Σ, T1 |= α, and T2 6|= α.
EL-TBoxes can be translated into directed hypergraphs by taking the
signature symbols as nodes and treating the axioms as hyperedges connecting
the nodes. For normalised EL-TBoxes, the axiom > v B is translated into
the hyperedge ({x>}, {xB}), the axiom A1 u . . . u An v B into the hyperedge
({xB1 , . . . , xBn }, {xA}), the axiom A v ∃r.B into the hyperedge ({xA}, {xr, xB}),
and the axiom ∃r.A v B into the hyperedge ({xr, xB}, {xA}), 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. In fact we can treat the ontology and its
hypergraph representation interchangeably. The existence of certain simulations
between hypergraphs for EL-terminologies characterises the fact that the
corresponding terminologies are logically equivalent and, thus, no logical difference
exists [
As the set cDiffΣ(T1, T2) is infinite in general, we make use of the following
“primitive witnesses” theorem from [
Example 1. Let T1 = {X ≡ A1 u A2, X v ∃r.>}, T2 = ∅, and let Σ = {A1, A2, r}. Note that T1 is not a terminology as the concept name X occurs twice on the left-hand side of an axiom. Then every difference α ∈ cDiffΣ(T1, T2) is equivalent to the inclusion A1 u A2 v ∃r.>. In particular, there does not exist a difference of the form ψ v θ, where ψ or θ is a concept name from Σ.
As illustrated by the example, we need to account for a new kind of differences C v C0 ∈ cDiffΣ(T1, T2) which are induced by a concept name X ∈ sig(T1) such that X 6∈ Σ, T1 |= C v X, and T1 |= X v C0. We obtain the following witness theorem for EL-TBoxes as an extension of the witness theorem for ELterminologies. Theorem 1 (Witness Theorem). Let T1, T2 be two normalised EL-TBoxes and let Σ be a signature. Then, cDiffΣ(T1, T2) 6= ∅ iff there exists an ELΣinclusion α = ϕ v ψ such that T1 |= α and T2 6|= α, where (i) ϕ is an ELΣ-concept and ψ = A ∈ Σ, (ii) ϕ = A ∈ Σ and ψ is an ELΣ-concept, or (iii) there exists X ∈ sig(T1) \ Σ such that T1 |= ϕ v X and T1 |= X v ψ.
The proof of the witness theorem for terminologies [
For deciding whether cDiffΣ(T1, T2) = ∅ in the case of general TBoxes, we now have to additionally consider differences of Type (iii). Differences of types (i) or (ii) can be checked by using forward or backward simulations adapted to normalised EL-TBoxes, respectively, whereas Type (iii) differences require a combination of both techniques.
Before we illustrate how Type (iii) differences can be dealt with, we first introduce some auxiliary notions. We define cWtnlΣhs(T1, T2) as the set of all concept names A from Σ such that there exists an ELΣ-concept C with A v C ∈ cDiffΣ(T1, T2). Similarly, cWtnrΣhs(T1, T2) is the set of all concept names A ∈ Σ such that there exists an ELΣ-concept C with C v A ∈ cDiffΣ(T1, T2). The concept names in cWtnlΣhs(T1, T2) are called left-hand side witnesses and the concept names in cWtnrΣhs(T1, T2) right-hand side witnesses. Additionally, we define cWtnmΣid(T1, T2) as the set of all concept names X from sig(T1) but not from Σ such that there exists C v C0 ∈ cDiffΣ(T1, T2) and T1 |= C v X and T1 |= X v C0. The concept names in cWtnmΣid(T1, T2) are called interpolating witnesses. To summarise, we have the following sets: cWtnlΣhs(T1, T2) = { A ∈ Σ | ∃ C ∈ ELΣ : A v C ∈ cDiffΣ(T1, T2) } cWtnrΣhs(T1, T2) = { A ∈ Σ | ∃ C ∈ ELΣ : C v A ∈ cDiffΣ(T1, T2) } cWtnmΣid(T1, T2) = { X ∈ sig(T1) \ Σ | ∃ C, C0 ∈ ELΣ : T1 |= C v X, T1 |= X v C0, T2 6|= C v C0 }
We illustrate the witness sets with the following example.
Example 2. Let T1 = {X ≡ A1 u A2, X v ∃r.>, A3 v A2, A3 v ∃r.A2}, T2 = {A2 v ∃r.>}, and let Σ = {A1, A2, r}. Then it holds that cWtnlΣhs(T1, T2) = {A3} (e.g. {A3 v A2, A3 v ∃r.A2} ⊆ cDiffΣ(T1, T2)), cWtnrΣhs(T1, T2) = {A2} (e.g. A3 v A2 ∈ cDiffΣ(T1, T2)), and cWtnmΣid(T1, T2) = {X} (e.g. T1 |= A1 u A3 v X, T1 |= X v ∃r.> and T2 6|= A1 u A3 v ∃r.>).
We obtain as a corollary of Theorem 2 that, to decide the logical difference between two EL-TBoxes, it is sufficient to check the emptiness of the witness sets.
Corollary 1. Let T1, T2 be two normalised EL-TBoxes and let Σ be a signature. Then it holds that cDiffΣ(T1, T2) = ∅ iff cWtnlΣhs(T1, T2) = cWtnrΣhs(T1, T2) = cWtnmΣid(T1, T2) = ∅.
To characterise an interpolating witness of a Type-(iii) difference, we use
the sets of its of subsumees and subsumers formulated using certain signature
symbols only. A similar approach was used for the construction of uniform
interpolants of E L-TBoxes in [
Definition 2. Let T be an E L-TBox, let Σ be a signature and let C be an E L-concept. We define PremisesTΣ (C) := { E ∈ E LΣ | T |= E v C } and ConclusionsΣ (C) := { E ∈ E LΣ | T |= C v E }.
T The set PremisesΣ (C) contains all E L-concepts formulated using Σ-symbols only
T that entail C w.r.t. T ; or are entailed by C in the case of ConclusionsΣ (C). The T elements of PremisesΣ (C) are also called Σ-implicants or Σ-subsumees of C
T w.r.t. T , and the elements of ConclusionsTΣ (C) are also named Σ-implicates or Σ-subsumers of C w.r.t. T .
In [
T T PremisesΣ (Y ). We aim now at lifting this result to general E L-TBoxes.
T Example 3. Let T1 = {A v X, ∃r.X v X, X v B1, X v B2} and T2 = {A v Y, ∃r.Y v Y 0, ∃r.Y 0 v Y, ∃r.Y v Z1, ∃r.Y v Z2, Y v B1, Y v B2, Z1 v B1, Z2 v B2} be two E L-TBoxes. Let Σ = {A, B1, B2, r} be a signature. Note that X in T1 is cyclic and intuitively, the interpretation of X in a model I of T1 contains all finite r-chains “ending in A”. In T2 the concept name Y is cyclic and its interpretation contains all r-chains ending in A that are of even length, whereas the interpretations of the concept names Z1 and Z2 contain all r-chains ending in A that are of odd length. Formally, we have that:
{A, ∃r.A, ∃r.∃r.A, . . . } ⊆ PremisesTΣ1 (X) {A, ∃r.∃r.A, ∃r.∃r.∃r.∃r.A, . . . } ⊆ PremisesTΣ2 (Y )
{∃r.A, ∃r.∃r.∃r.A, . . . } ⊆ PremisesTΣ2 (Zi) for i ∈ {1, 2} In particular, for i ∈ {1, 2}, we have
PremisesTΣ1 (X) = PremisesTΣ2 (Y ) ∪ PremisesTΣ2 (Zi).
Intuitively, the set of Σ-implicants of X in T1 are distributed over the concept names Y and Zi in T2. Moreover it holds that
ConclusionsTΣ1 (X) = ConclusionsTΣ2 (Y ) = ConclusionsTΣ2 (Z1 u Z2). The concept name X in T1 could be forward simulated either by Y or Z1 u Z2 in T2. Note that Z1 or Z2 individually are not sufficient. Analogously, X could be backward simulated by Y t Z1 or Y t Z2. None of the concept names X, Z1, or Z2 are sufficient individually for the backward simulation. Combining backward and forward simulation, X could be simulated by Y t (Z1 u Z2).
In general, we hypothesise that non-Σ-concept names X in T1 need to be “simulated” by concepts of the form Fin=1 Ci, where Ci are E L-concepts.
We now show how fixpoint reasoning can be used to find difference witnesses between general EL-TBoxes.
Given Theorem 2, we know that any difference C v C0 ∈ cDiffΣ(T1, T2), for two ELΣ-concepts C and C0, is connected to some concept name X occurring in T1 for which either T1 |= C v X, or T1 |= X v C0 (or both) holds. To check whether X is indeed a difference witness, we construct concepts BTΣ1 (X) and FTΣ1 (X) formulated in ELU μΣ and in ELν , respectively, to describe the (potenΣ tially infinite) disjunction of Σ-concepts that are subsumed by X w.r.t. T1, and the conjunction of all the Σ-concepts that subsume X w.r.t. T1, respectively. Note that the use of fixpoint allows for a finite description of infinite disjunctions or conjunctions. The ELU μΣ-concept BTΣ1 (X) hence is a finite representation of the set PremisesTΣ1 (X), whereas the ELνΣ-concept FTΣ1 (X) represents the set PremisesTΣ1 (X) in a finite way. Using the fixpoint descriptions of the premises and conclusions of X w.r.t. T1, we can verify whether X is a difference witness by checking T2 |= BTΣ1 (X) v FTΣ1 (X).
We first turn our attention to the set PremisesTΣ1 (X). Before we can give a formal definition for the concept BTΣ1 (X), we have to introduce the following auxiliary notion to handle concept names X in the definition of BTΣ1 (X) for which there exist axioms of the form Z1 u . . . u Zn v Z in a normalised TBox T such that T |= Z v X. Intuitively, given a concept name X, we construct a set ConjT (X) containing sets of concept names which has the property that for every EL-concept D with T |= D v X, there exists a set S = {Y1, . . . , Ym} ∈ ConjT (X) such that T |= D v Yi follows without involving any axioms of the form Z1 u . . . u Zn v Z. Nested implications between such axioms also have to be taken into account.
Definition 3. Let T be a normalised EL-TBox and let X ∈ NC. We define the set ConjT (X) ⊆ 2sig(T )∩NC to be smallest set inductively defined as follows: – {X} ∈ ConjT (X); – if S ∈ ConjT (X), Y ∈ S, and Z1 u . . . u Zn v Z ∈ T such that n ≥ 2 and T |= Z v Y , then S \ {Y } ∪ {Z1, . . . , Zn} ∈ ConjT (X).
Note that for every concept name X the set ConjT (X) is finite as sig(T ) ∩ NC is finite.
Example 4. Let T1 = {A v X, ∃r.X v X}. Then ConjT1 (X) = {{X}}. For T2 = {X1 u X2 v X, X3 u X4 v X1, Y1 u Y2 v X}, we have that
ConjT2 (X) = {{X}, {X1, X2}, {X3, X4, X2}, {Y1, Y2}}.
We can now give a formal definition of the concept BΣ(X).
T Definition 4. Let T be a normalised EL-TBox, let Σ be a signature, and let μ X ∈ sig(T ). For a mapping η : NC → NV, we define a closed ELU Σ-concept BTΣ(X, η) as follows. We set BTΣ(X, η) = > if T |= > v X; otherwise BTΣ(X, η) is defined recursively in the following way: – If X ∈ dom(η), then – If X 6∈ dom(η), we set
BΣ(X, η) = η(X)
T
G S∈ConjT (X)
S={Y1,...,Ym} BΣ(X, η) = μx.
T (Y10 u . . . u Y m0) where x is a fresh variable, and Yi0 (1 ≤ i ≤ n) is defined as follows for η0 := η ∪ {X 7→ x}:
Yi0 =
G T |=BvYi
B∈Σ
B t
G ∃r.Zrv∈ΣY ∈T T |=Y vYi ∃r.BTΣ(Z, η0) Finally, we set BΣ(X) = BΣ(X, ∅).
T T Intuitively, the construction of BΣ(X) starts from X and recursively collects
T all the concept names contained in Σ and all the left-hand sides of axioms in T that could be relevant for X to be entailed by a concept w.r.t. T . By taking into account all possible axioms that could lead to a logical entailment, it is guaranteed that we capture every Σ-concept from which X follows w.r.t. T . Reasoning involving axioms of the form Z1 u . . . u Zn v Z is handled by the set ConjT (X). Infinite recursion over concepts of the form ∃r.C is avoided by keeping track of the concept names that been visited already using the mapping η.
We note that for a normalised EL-terminology T , the concept BTΣ(X) is of a simpler form than for normalised EL-TBoxes. This is because the concept name X can occur on the right-hand side of at most one axiom of the form ∃r.A v X or A1 u . . . u An v X with n ≥ 2 in T , whereas in a TBox several such axioms may occur.
We illustrate the concept BΣ(X) with the following examples.
T Example 5. Let T1 = {A1 u A2 v X, A3 v A2, ∃r.A2 v A1, ∃r.A2 v X}, T2 μ= T1 ∪ {∃r.X v A2}, and let Σ = {A1, A2, A3, r}. We obtain the following ELU Σconcepts. We write ϕ instead of μx.ϕ if x does not occur freely in ϕ.
BTΣ1 (A1) = A1 t ∃r.(A2 t A3)
BTΣ1 (A2) = A2 t A3 BTΣ1 (X) = ((A1 t ∃r.(A2 t A3)) u (A2 t A3)) t ∃r.(A2 t A3) BTΣ2 (X) = μx.(((A1 t ∃r.(A2 t A3 t ∃r.x)) u (A2 t A3 t ∃r.x))
t ∃r.(A2 t A3 t ∃r.x)) Example 6. Let T1, T2 be defined as in Example 3, and let Σ = {A, B1, B2, r}. We have that for i ∈ {1, 2}:
BTΣ1 (X) = μx.(A t ∃r.x) BTΣ2 (Y ) = μy.(A t ∃r.∃r.y)
BTΣ1 (Bi) = Bi t A t ∃r.μx.(A t ∃r.x)
BTΣ2 (Zi) = ∃r.μy.(A t ∃r.∃r.y) BTΣ2 (Bi) = Bi t A t ∃r.μy1.(∃r.(A t ∃r.y1)) t ∃r.μy2.(A t ∃r.∃r.y2) By inspecting Definition 4 it is easy to see that |= BΣ (X) ≡ ⊥ if there does T not an E LΣ -concept C with T |= C v X. Overall, one can establish the following correctness and completeness properties.
Lemma 1. Let T be a normalised E L-TBox, let Σ be a signature, and let X ∈ sig(T ). Then the E LU μΣ -concept BΣ (X) satisfies the following properties:
T (i) T |= BΣ (X) v X, and
T (ii) for every D ∈ PremisesΣ (X),
T T |= D v X iff |= D v BΣ (X).
T
The following lemma states that the E LU μ-concept BΣ (X) exactly captures the infinite set PremisesΣ (X). More formally, the concept TBΣ (X) is equivalent to
T T the infinite disjunction over all the concepts contained in the set PremisesΣ (X). T Lemma 2. Let T be a normalised E L-TBox, let Σ be a signature, and let X ∈ sig(T ). Then for every interpretation I it holds that (BTΣ (X))I,∅ = [{ CI,∅ | C ∈ PremisesΣ (X) }.
T Analogously to the concept BΣ (X), it is possible to construct an E Lν Σ concept FTΣ (X) which exactly captTures the set ConclusionsTΣ (X) for a concept name X and an E L-TBox T . Due to lack of space, we cannot give a full definition of the concept FΣ (X). Instead, we state its existence and its essential property
T in the following lemma.
Lemma 3. Let T be a normalised E L-TBox, let Σ be a signature, and let X ∈ sig(T ). Then there exists an E Lν -concept FΣ (X) such that for every interT pretation I it holds that (FTΣ (X))I,∅ = [{ CI,∅ | C ∈ ConclusionsΣ (X) }.
T
We can now state the following theorem, which establishes how the concepts BΣ (X) and FΣ (X) can be used to search for difference witnesses.
T T Theorem 2. Let T1, T2 be two normalised E L-TBoxes. Then it holds that: (i) A 6∈ cWtnlΣhs(T1, T2) iff T2 |= A v FTΣ1 (A), for every A ∈ Σ; (ii) A 6∈ cWtnrΣhs(T1, T2) iff T2 |= BTΣ1 (A) v A, for every A ∈ Σ; and (iii) X 6∈ cWtnmΣid(T1, T2) iff T2 |= BTΣ1 (X) v FTΣ1 (X), for every X ∈ sig(T1) \ Σ.
Theorem 2 together with Corollary 1 give rise to an algorithm for deciding the
logical difference between E L-TBoxes. Procedure 1 is such an algorithm based
on reasoning in the hybrid μ-calculus, which allows for fixpoint reasoning w.r.t.
TBoxes [
Theorem 3. Procedure 1 runs in ExpTime.
Procedure 1 Deciding existence of logical difference
Input: Normalised EL-TBoxes T1, T2 and signature Σ
Output: true or false
1: for every concept name X ∈ sig(T1) ∪ Σ do
2: B := BTΣ1 (X)
3: F := FTΣ1 (X)
4: if X ∈ Σ then
5: if T2 6|= X v F or T2 6|= B v X then
6: return true
7: end if
8: else if T2 6|= B v F then
9: return true
10: end if
11: end for
12: return false
We note that the lower bound for the running time of Procedure 1 may also be
exponential as the underlying problem of deciding the logical difference of two
EL-TBoxes is ExpTime-complete [
Example 7. Continue Example 3, where sig(T1) ∪ Σ = {A, X, B1, B2, r}. For A, B = BTΣ1 (A) = A, and F = FTΣ1 (A) = B1 u B2. As T2 |= A v F and T2 |= B v A, the loop continues. Then for X, B = BTΣ1 (X) = μx.(A t ∃r.x) and F = FTΣ1 (X) = B1 u B2 (cf. Example 6). Since it holds that T2 |= B v F , the loop continues. For B1, B = B1 t A t ∃r.μx.(A t ∃r.x) and F = B1. As T2 |= B1 v F and T2 |= B v B1, the loop continues. The case of B2 is similar to that of B1. Finally, the algorithm returns false.
Procedure 1 can be modified to obtain witnesses to difference subsumption. Example 8. We run Procedure 1 on T1, T3 = T2 \{Z1 v B1} and Σ, where T1, T2 and Σ are the same as in Example 3. Then, for X, we have that B = BTΣ1 (X) = μx.(A t ∃r.x) and F = FTΣ1 (X) = B1 u B2. However, T3 6|= B v F , which means X ∈ cWtnmΣid(T1, T3). Similarly, it can readily be seen that B1 ∈ cWtnrΣhs(T1, T3). 5
We have revisited our solution to logical difference problem for EL-terminologies
which was based on finding simulations between hypergraph representations of
the terminologies [