=Paper=
{{Paper
|id=None
|storemode=property
|title=Hybrid EL-Unification is NP-complete
|pdfUrl=https://ceur-ws.org/Vol-1014/paper_9.pdf
|volume=Vol-1014
|dblpUrl=https://dblp.org/rec/conf/dlog/BaaderGM13
}}
==Hybrid EL-Unification is NP-complete==
https://ceur-ws.org/Vol-1014/paper_9.pdf
Hybrid EL-Unification is NP-complete
Franz Baader, Oliver Fernández Gil, and Barbara Morawska?
{baader,morawska}@tcs.inf.tu-dresden.de, olitof11@gmail.com
Theoretical Computer Science, TU Dresden, Germany
Abstract Unification in Description Logics (DLs) has been proposed as
an inference service that can, for example, be used to detect redundan-
cies in ontologies. For the DL EL, which is used to define several large
biomedical ontologies, unification is NP-complete. However, the unifi-
cation algorithms for EL developed until recently could not deal with
ontologies containing general concept inclusions (GCIs). In a series of re-
cent papers we have made some progress towards addressing this prob-
lem, but the ontologies the developed unification algorithms can deal
with need to satisfy a certain cycle restriction. In the present paper, we
follow a different approach. Instead of restricting the input ontologies,
we generalize the notion of unifiers to so-called hybrid unifiers. Whereas
classical unifiers can be viewed as acyclic TBoxes, hybrid unifiers are
cyclic TBoxes, which are interpreted together with the ontology of the
input using a hybrid semantics that combines fixpoint and descriptive
semantics. We show that hybrid unification in EL is NP-complete.
1 Introduction
The DL EL, which offers the constructors conjunction (u), existential restriction
(∃r.C), and the top concept (>), has recently drawn considerable attention since,
on the one hand, important inference problems such as the subsumption problem
are polynomial in EL, even in the presence of GCIs [9]. On the other hand, though
quite inexpressive, EL can be used to define biomedical ontologies, such as the
large medical ontology SNOMED CT.1 From a semantic point of view, concept
names and concept descriptions represent sets of individuals, whereas role names
represent binary relations between individuals. For example, using the concept
names Head_injury and Severe, and the role names finding and status, we can
describe the concept of a patient with severe head injury as
Patient u ∃finding.(Head_injury u ∃status.Severe). (1)
In a DL ontology, one can use concept definitions to introduce abbreviations
for concept descriptions. For example, we could use the definition Head_injury ≡
Injury u ∃finding_site.Head to define Head_injury as an injury that is located at
?
Supported by DFG under grant BA 1122/14-2
1
see http://www.ihtsdo.org/snomed-ct/
the head. More generally, GCIs can be used to require that certain inclusions
hold in all models of the ontology. For example,
∃finding.∃status.Severe v ∃status.Emergency (2)
is a GCI that says that a severe finding entails an emergency status.
Knowledge representation systems based on DLs provide their users with
various inference services that allow them to deduce implicit knowledge from
the explicitly represented knowledge. For instance, the subsumption algorithm
allows one to determine subconcept-superconcept relationships. For example,
the concept description (1) is subsumed by (i.e., is a subconcept of) the concept
description ∃finding.∃status.Severe. With respect to the GCI (2), it is thus also
subsumed by ∃status.Emergency, i.e., in all models of this GCI, patients with
severe head injury have an emergency status.
Unification in DLs has been proposed in [8] as a non-standard inference
service that can, for instance, be used to detect redundancies in ontologies. For
example, assume that one developer of a medical ontology describes the concept
of a patient with severe head injury using the concept description (1), whereas
another one represents it as
Patient u ∃finding.(Severe_injury u ∃finding_site.Head). (3)
These two concept descriptions are not equivalent, but they are nevertheless
meant to represent the same concept. They can obviously be made equivalent
by introducing definitions for the concept names Head_injury and Severe_injury:
if we define Head_injury ≡ Injury u ∃finding_site.Head and Severe_injury ≡
Injury u ∃status.Severe, then the two concept descriptions (1) and (3) are equiva-
lent w.r.t. these definitions. If such definitions exist, we say that the descriptions
are unifiable, and call the TBox consisting of these definitions a unifier. In the
standard definition of unification in DLs, it is required that this TBox is acyclic,
i.e., there are no cyclic dependencies between the definitions.
To motivate our interest in unification w.r.t. GCIs, assume that the second
developer uses the description
Patient u ∃status.Emergency u ∃finding.(Severe_injury u ∃finding_site.Head)(4)
instead of (3). The descriptions (1) and (4) are not unifiable without additional
GCIs, but they are unifiable, with the same unifier as above, if the GCI (2) is
present in a background ontology.
In [6], we were able to show that unification in the DL EL (without back-
ground ontology) is NP-complete. In addition to a brute-force “guess and then
test” NP-algorithm [6], we have also developed a goal-oriented unification algo-
rithm for EL, in which nondeterministic decisions are only made if they are trig-
gered by “unsolved parts” of the unification problem [7]. In [7] it was also shown
that these two approaches for unification of EL-concept descriptions (without
any background ontology) can easily be extended to the case of an acyclic TBox
as background ontology without really changing the algorithms or increasing
their complexity. For more general GCIs, such a simple solution is no longer
possible.
In [3], we extended the brute-force “guess and then test” NP-algorithm from
[6] to the case of GCIs. Unfortunately, the algorithm is complete only for ontolo-
gies that satisfy a certain restriction on cycles, which, however, does not prevent
all cycles. For example, the cyclic GCI ∃child.Human v Human satisfies this re-
striction, whereas the cyclic GCI Human v ∃parent.Human does not. In [4], we
introduced a more practical, goal-oriented unification algorithm that can also
deal with role hierarchies and transitive roles, but still needs the ontology (now
consisting of GCIs and role axioms) to be cycle-restricted. At the moment, it is
not clear how similar brute-force or goal-oriented algorithms could be obtained
for the general case without cycle-restriction.
In this paper, we follow another line of attack on this problem. Instead of
restricting the input ontology, we allow cyclic TBoxes to be used as unifiers.
Subsumption w.r.t. cyclic TBoxes in EL has been investigated in detail in [1].
In addition to the classical descriptive semantics, it also makes sense to use
greatest fixpoint semantics (gfp-semantics) for such TBoxes. For example, w.r.t.
this semantics, the definition X ≡ ∃parent.X describes exactly those domain
elements that are the origin of an infinite parent-chain, whereas descriptive se-
mantics would also allow the empty set to be an interpretation of X, even if
there are infinite parent-chains. Hybrid semantics deals with the case where a
TBox interpreted with gfp-semantics is combined with GCIs that are interpreted
with descriptive semantics [10,12]. Its introduction was originally motivated by
the fact that the least common subsumer (lcs) w.r.t. a set of GCIs interpreted
with descriptive semantics need not exist. For example, w.r.t. the GCIs
Human v ∃parent.Human and Horse v ∃parent.Horse, (5)
there is no least concept description (w.r.t. subsumption) that subsumes both
Human and Horse. What elements of these two concepts have in common is that
they are the origin of an infinite parent-chain, and thus the concept X with
definition X ≡ ∃parent.X is their lcs, if we interpret this definition with gfp-
semantics, but the GCIs (5) still with descriptive semantics. A hybrid unifier is
a cyclic TBox that, together with the background ontology consisting of GCIs,
entails the unification problem w.r.t. hybrid semantics. We will show that hybrid
unification in EL, i.e., the problem of testing whether a hybrid unifier exists, is
NP-complete. The proofs, which can be found in [5], are based on the proof
system for hybrid subsumption introduced in [12].
2 The Description Logic EL
The expressiveness of a DL is determined both by the formalism for describing
concepts (the concept description language) and the terminological formalism,
which can be used to state additional constraints on the interpretation of con-
cepts in a so-called ontology.
The concept description language The concept description language con-
sidered in this paper is called EL. Starting with a finite set NC of concept names
and a finite set NR of role names, EL-concept descriptions are built from concept
names using the constructors conjunction (C u D), existential restriction (∃r.C
for every r ∈ NR ), and top (>). Since in this paper we only consider EL-concept
descriptions, we will usually dispense with the prefix EL.
On the semantic side, concept descriptions are interpreted as sets. To be
more precise, an interpretation I = (∆I , ·I ) consists of a non-empty domain ∆I
and an interpretation function ·I that maps concept names to subsets of ∆I and
role names to binary relations over ∆I . This function is inductively extended to
concept descriptions as follows:
>I := ∆I , (C u D)I := C I ∩ DI , (∃r.C)I := {x | ∃y : (x, y) ∈ rI ∧ y ∈ C I }
Classical ontologies and subsumption A concept definition is an expression
of the form X ≡ C where X is a concept name and C is a concept description,
and a general concept inclusion (GCI) is an expression of the form C v D,
where C, D are concept descriptions. An interpretation I is a model of this
concept definition (this GCI) if it satisfies X I = C I (C I ⊆ DI ). This semantics
for GCIs and concept definitions is usually called descriptive semantics.
A TBox is a finite set T of concept definitions that does not contain multiple
definitions, i.e., {X ≡ C, X ≡ D} ⊆ T implies C = D. Note that we do not
prohibit cyclic dependencies among the concept definitions in a TBox, i.e., when
defining a concept X we may (directly or indirectly) refer to X. An acyclic TBox
is a TBox without cyclic dependencies. An ontology is a finite set of GCIs. The
interpretation I is a model of a TBox (ontology) iff it is a model of all concept
definitions (GCIs) contained in it.
A concept description C is subsumed by a concept description D w.r.t. an
ontology O (written C vO D) if every model of O is also a model of the GCI
C v D. We say that C is equivalent to D w.r.t. O (C ≡O D) if C vO D
and D vO C. As shown in [9], subsumption w.r.t. EL-ontologies is decidable in
polynomial time.
Note that TBoxes can be seen as special kinds of ontologies since concept
definitions X ≡ C can of course be expressed by GCIs X v C, C v X. Thus, the
above definition of subsumption also applies to TBoxes. However, in our hybrid
ontologies we will interpret concept definitions using greatest fixpoint semantics
rather than descriptive semantics.
Hybrid ontologies We assume in the following that the set of concept names
NC is partitioned into the set of primitive concepts Nprim and the set of defined
concepts Ndef . In a hybrid TBox, concept names occurring on the left-hand side
of a concept definition are required to come from the set Ndef , whereas GCIs
may not contain concept names from Ndef .
Definition 1 (Hybrid EL-ontologies). A hybrid EL-ontology is a pair (O, T ),
where O is an EL-ontology containing only concept names from Nprim , and T is
a (possibly cyclic) EL-TBox such that X ≡ C ∈ T for some concept description
C iff X ∈ Ndef .
The idea underlying the definition of hybrid ontologies is the following: O can be
used to constrain the interpretation of the primitive concepts and roles, whereas
T tells us how to interpret the defined concepts occurring in it, once the inter-
pretation of the primitive concepts and roles is fixed.
A primitive interpretation J is defined like an interpretation, with the only
difference that it does not provide an interpretation for the defined concepts. A
primitive interpretation can thus interpret concept descriptions built over Nprim
and NR , but it cannot interpret concept descriptions containing elements of
Ndef . Given a primitive interpretation J , we say that the (full) interpretation
I is based on J if it has the same domain as J and its interpretation function
coincides with J on Nprim and NR .
Given two interpretations I1 and I2 based on the same primitive interpreta-
tion J , we define I1 J I2 iff X I1 ⊆ X I2 for all X ∈ Ndef .
It is easy to see that the relation J is a partial order on the set of interpre-
tations based on J . In [1] the following was shown: given an EL-TBox T and a
primitive interpretation J , there exists a unique model I of T such that
– I is based on J ;
– I 0 J I for all models I 0 of T that are based on J .
We call such a model I a gfp-model of T .
Definition 2 (Semantics of hybrid EL-ontologies). The interpretation I is
a hybrid model of the hybrid EL-ontology (O, T ) iff I is a gfp-model of T and
the primitive interpretation J it is based on is a model of O.
It is well-known that gfp-semantics coincides with descriptive semantics for
acyclic TBoxes. Thus, if T is actually acyclic, then I is a hybrid model of (O, T )
according to the semantics introduced in Definition 2 iff it is a model of T ∪ O
w.r.t. descriptive semantics, i.e., iff I is a model of every GCI in O and of every
concept definition in T .
Subsumption w.r.t. hybrid EL-ontologies Let (O, T ) be a hybrid EL-
ontology and C, D EL-concept descriptions. Then C is subsumed by D w.r.t.
(O, T ) (written C vgfp,O,T D) iff every hybrid model of (O, T ) is also a model
of the GCI C v D. As shown in [10,12], subsumption w.r.t. hybrid EL-ontologies
is also decidable in polynomial time.
Here, we sketch the proof-theoretic approach for deciding subsumption from
[12] since our algorithms for hybrid unification in EL are based on it. The proof
calculus is parametrized with a hybrid EL-ontology (O, T ) and a finite set of
GCIs ∆ for which we want to decide subsumption. A sequent for (O, T ) and ∆
is of the form C vn D, where C, D are sub-descriptions of concept descriptions
occurring in O, T , and ∆, and n ≥ 0. If (O, T ) and ∆ are clear from the context,
we will sometimes simply say sequent without specifying (O, T ) and ∆ explicitly.
C vn C (Refl) C vn > (Top) C v0 D (Start)
C vn E D vn E C vn D C vn E
C u D vn E (AndL1) C u D vn E (AndL2) C vn D u E (AndR)
C vn D
∃r.C vn ∃r.D (Ex)
C vn D D vn C C vn E F vn D
X vn D (DefL) D vn+1 X (DefR) C vn D (GCI)
for X ≡ C ∈ T for X ≡ C ∈ T for E v F ∈ O
Figure 1. The calculus HC(O, T , ∆).
The rules of the Hybrid EL-ontology Calculus HC(O, T , ∆) are depicted in
Fig. 1. Again, if (O, T ) and ∆ are clear from the context, we will sometimes
dispense with specifying them explicitly and just talk about the calculus HC.
The rules of this calculus can be used to derive new sequents from sequents that
have already been derived. For example, the sequents in the first row of the figure
can always be derived without any prerequisites, using the rules (Refl), (Top),
and (Start), respectively. Using the rule (AndR), the sequent C vn D u E can
be derived in case both C vn D and C vn E have already been derived. Note
that the rule Start applies only for n = 0. Also note that, in the rule (DefR),
the index is incremented when going from the prerequisite to the consequent.
A derivation in HC(O, T , ∆) can be represented in an obvious way by a proof
tree whose nodes are sequents: a proof tree for C vn D has this sequent as its
root, instances of the rules Refl, Top, and Start as leaves, and each parent-child
relation corresponds to an instance of a rule of HC other than Refl, Top, and
Start (see [12] for more details)
Definition 3. Let C, D be sub-descriptions of concept descriptions occurring in
O, T , and ∆. Then we say that C v∞ D can be derived in HC(O, T , ∆) if all
sequents C vn D for n ≥ 0 can be derived using the rules of HC(O, T , ∆).
The calculus HC is sound and complete for subsumption w.r.t. hybrid EL-
ontologies in the following sense.
Theorem 4 (Soundness and Completeness of HC). Let (O, T ) be a hybrid
EL-TBox, ∆ a finite set of GCIs, and C, D sub-descriptions of concept descrip-
tions occurring in O, T , and ∆. Then C vgfp,O,T D iff C v∞ D can be derived
in HC(O, T , ∆).
In [12], soundness and completeness of HC is actually formulated for a restricted
setting where ∆ is empty and C, D are elements of Ndef that occur as left-hand
sides in T . It is, however, easy to see that the proof given in [12] generalizes to
the above theorem.
For n ∈ N∪{∞}, we collect the GCIs C v D such that C vn D is derivable in
HC(O, T , ∆) in the set Dn (O, T , ∆). Obviously, D0 (O, T , ∆) consists of all GCIs
built from sub-descriptions of concept descriptions occurring in O, T , and ∆, and
it is not hard to show that Dn+1 (O, T , ∆) ⊆ Dn (O, T , ∆) holds for all n ≥ 0 [12].
Thus, to compute D∞ (O, T , ∆), one can start with D0 (O, T , ∆), and then com-
pute D1 (O, T , ∆), D2 (O, T , ∆), . . ., until Dm+1 (O, T , ∆) = Dm (O, T , ∆) holds
for some m ≥ 0, and thus Dm (O, T , ∆) = D∞ (O, T , ∆). Since the cardinality
of the set of sub-descriptions is polynomial in the size of the input O, T , and
∆, the computation of each set Dn (O, T , ∆) can be done in polynomial time,
and we can be sure that only polynomially many such sets need to be computed
until an m with Dm+1 (O, T , ∆) = Dm (O, T , ∆) is reached. This shows that the
calculus HC(O, T , ∆) indeed yields a polynomial-time subsumption algorithm
(see [12] for details).
3 Hybrid unification in EL
We will first introduce the new notion of hybrid unification and then relate it to
the notion of unification in EL w.r.t. background ontologies considered in [3,4].
Definition 5. Let O be an EL-ontology containing only concept names from
Nprim . An EL-unification problem w.r.t. O is a finite set of GCIs Γ = {C1 v
D1 , . . . , Cn v Dn } (which may also contain concept names from Ndef ). The
TBox T is a hybrid unifier of Γ w.r.t. O if (O, T ) is a hybrid EL-ontology that
entails all the GCIs in Γ , i.e. , C1 vgfp,O,T D1 , . . . , Cn vgfp,O,T Dn . We call
such a TBox T a classical unifier of Γ w.r.t. O if it is acyclic.
It is easy to see that the notion of a classical unifier indeed corresponds to
the notion of a unifier introduced in [3,4]. In fact, Nprim and Ndef respectively
correspond to the sets of concept constants and concept variables in previous
papers on unification in DLs. Using acyclic TBoxes rather than substitutions as
unifiers is also not a relevant difference. As explained in [2], by unfolding concept
definitions, the acyclic TBox T can be transformed into a substitution σT such
that Ci vT ∪O Di iff σT (Ci ) vO σT (Di ). Conversely, replacements X 7→ E of a
substitution σ can be expressed as concept definitions X ≡ E in a corresponding
acyclic TBox. In contrast, hybrid unifiers cannot be translated into substitutions
since the unfolding process would not terminate for a cyclic TBox.
Obviously, any classical unifier is a hybrid unifier, but the converse need
not hold. The following is an example of an EL-unification problem w.r.t. a
background ontology that has a hybrid unifier, but no classical unifier.
Example 6. Let O be the ontology consisting of the GCIs (5), and
Γ := {Human v X, Horse v X, X v ∃parent.X},
where X ∈ Ndef and Human, Horse ∈ Nprim . Intuitively, this unification problem
asks for a concept such that all horses and humans belong to this concept and
every element of it has a parent also belonging to it. It is easy to see that
T := {X ≡ ∃parent.X} is a hybrid unifier of Γ w.r.t. O. In fact, we have already
mentioned in the introduction that X is then the lcs of Human and Horse, and
obviously the hybrid ontology (O, T ) also entails the third GCI in Γ . It is also
not hard to show that this unification problem does not have a classical unifier,
basically for the same reasons that Human and Horse do not have an EL-concept
description as lcs (see [5] for details).
Flat unification problems To simplify the technical development, it is con-
venient to normalize the unification problem appropriately. To introduce this
normal form, we need the notion of an atom. An atom is a concept name or
an existential restriction. Obviously, every EL-concept description C is a finite
conjunction of atoms, where > is considered to be the empty conjunction. An
atom is called flat if it is a concept name or an existential restriction of the form
∃r.A for a concept name A.
The GCI C v D is called flat if C is a conjunction of n ≥ 0 flat atoms and
D is a flat atom. The unification problem Γ w.r.t. the ontology O is called flat
if both Γ and O consist of flat GCIs.
Given a unification problem Γ w.r.t. an ontology O, we can compute in
polynomial time (see [5]) a flat ontology O0 and a flat unification problem Γ 0
such that Γ has a (hybrid or classical) unifier w.r.t. O iff Γ 0 has a (hybrid or
classical) unifier w.r.t. O0 . For this reason, we will assume in the following that
all unification problems are flat.
Local unifiers The main reason why EL-unification without background on-
tologies is in NP is that any unification problem that has a unifier also has a
local unifier. For classical unification w.r.t. background ontologies this is only
true if the background ontology is cycle-restricted.
Given a flat unification problem Γ w.r.t. an ontology O, we denote by At
the set of atoms occurring as sub-descriptions in GCIs in Γ or O. The set of
non-variable atoms is defined as by Atnv := At \ Ndef . Though the elements of
Atnv cannot be defined concepts, they may contain defined concepts if they are
of the form ∃r.X for some role r and a concept name X ∈ Ndef .
In order to define local unifiers, we consider assignments ζ of subsets ζX of
Atnv to defined concepts X ∈ Ndef . Such an assignment induces a TBox
l
Tζ := {X ≡ D | X ∈ Ndef }.
D∈ζX
We call such a TBox local. The (hybrid or classical) unifier T of Γ w.r.t. O is
called local unifier if T is local, i.e., there is an assignment ζ such that T = Tζ .
As shown in [3], there are unification problems that have a classical unifier,
but no local classical unifier.
Example 7. Let O = {B v ∃s.D, D v B} and consider the unification problem
Γ := {A1 u B v Y1 , Y1 v A1 u B, A2 u B v Y2 , Y2 v A2 u B,
∃s.Y1 v X, ∃s.Y2 v X, X v ∃s.X},
where A1 , A2 , B ∈ Nprim and X, Y1 , Y2 ∈ Ndef . This problem has the classical
unifier T := {Y1 ≡ A1 u B, Y2 ≡ A2 u B, X ≡ ∃s.B}, which is not local since it
uses the atom ∃s.B. As shown in [3], Γ actually does not have a local classical
unifier w.r.t. O. However, it is easy to see that T := {Y1 ≡ A1 u B, Y2 ≡
A2 u B, X ≡ ∃s.X} is a local hybrid unifier of T . In fact, gfp-semantics applied
to T ensures that X consists of exactly those domain elements that are the origin
of an infinite s-chain, and O ensures that any element of B (and thus also of
∃s.B) is the origin of an infinite s-chain.
To overcome the problem of missing local unifiers, the notion of a cycle-
restricted ontology was introduced in [3]: the EL-ontology O is called cycle-
restricted if there is no nonempty sequence r1 , . . . , rn of role names and EL-
concept description C such that C vO ∃r1 . · · · ∃rn .C. Note that the ontology O
of Example 7 is not cycle-restricted since B vO ∃s.B.
The main technical result shown in [3] is that any EL-unification problem
Γ that has a classical unifier w.r.t. the cycle-restricted ontology O also has a
local classical unifier. This yields the following brute-force algorithm for classical
EL-unification w.r.t. cycle-restricted ontologies: first guess an acyclic local TBox
T , and then check whether T is indeed a unifier of Γ w.r.t. O. As shown in [3],
this algorithm runs in nondeterministic polynomial time. NP-hardness follows
from the fact that already classical unification in EL w.r.t. the empty ontology
is NP-hard [6].
4 Hybrid EL-unification is NP-complete
The fact that hybrid EL-unification w.r.t. arbitrary EL-ontologies is in NP is an
easy consequence of the following proposition.
Proposition 8. Consider a flat EL-unification problem Γ w.r.t. an EL-ontology
O. If Γ has a hybrid unifier w.r.t. O then it has a local hybrid unifier w.r.t. O.
In fact, the NP-algorithm simply guesses a local TBox and then checks (using
the polynomial-time algorithm for hybrid subsumption) whether it is a hybrid
unifier.
To prove the proposition, we assume that T is a hybrid unifier of Γ w.r.t. O.
We use this unifier to define an assignment ζ T as follows:
T
ζX := {D ∈ Atnv | X vgfp,O,T D}.
Let T 0 be the TBox induced by this assignment. To show that T 0 is indeed a
hybrid unifier of Γ w.r.t. O, we consider the set of GCIs
∆ := {C1 u . . . u Cm v D | C1 , . . . , Cm , D ∈ At},
and prove that, for any GCI C1 u . . . u Cm v D ∈ ∆, derivability of C1 u . . . u
Cm v∞ D in HC(O, T , ∆) implies derivability of C1 u . . . u Cm v∞ D also in
HC(O, T 0 , ∆). Soundness and completeness of HC, together with the facts that
Γ ⊆ ∆ and T is a hybrid unifier of Γ w.r.t. O, then imply that T 0 is also a
hybrid unifier of Γ w.r.t. O. Thus, to complete the proof of Proposition 8, it is
enough to prove the following lemma.
Lemma 9. Let C1 u . . . u Cm v D ∈ ∆. If C1 u . . . u Cm v∞ D is derivable
in HC(O, T , ∆), then C1 u . . . u Cm vn D is derivable in HC(O, T 0 , ∆) for all
n ≥ 0.
Proof. We prove derivability of C1 u. . .uCm vn D in HC(O, T 0 , ∆) by induction
on n. The base case is trivial due to the rule (Start).
Induction Step: We assume that the statement of the lemma holds for n −
1, and show that it then also holds for n. Let ` be such that D` (O, T , ∆) =
D∞ (O, T , ∆). We know that there exists a proof tree P for C1 u . . . u Cm v` D
in HC(O, T , ∆). Consider the subtree of P that is obtained from it by cutting
branches at the nodes obtained by an application of one of the rules (DefL) or
(DefR). The tree obtained this way contains only sequents with index ` and has
as its leaves
– instances of the rules (Refl), (Top), or (Start),
– consequences E1 v` E2 of instances of the rules (DefL) or (DefR).
In order to show that C1 u . . . u Cm vn D is derivable in HC(O, T 0 , ∆), it is
sufficient to show that, for leaves E1 v` E2 of the second kind, E1 vn E2 is
derivable in HC(O, T 0 , ∆) (see [5] for details).
First, assume that E1 v` E2 was obtained by an application of (DefR).
T
Then E2 ∈ Ndef . Assume that ζE 2
= {F1 , . . . , Fq }. By the definition of ζ T ,
we have E2 vgfp,O,T Fi for all i, 1 ≤ i ≤ q. In addition, by our choice of `,
derivability of E1 v` E2 in HC(O, T , ∆) (using the subtree of P with this node
as root) yields E1 vgfp,O,T E2 , and thus E1 vgfp,O,T Fi for all i, 1 ≤ i ≤ q.
Consequently, E1 v∞ Fi is derivable in HC(O, T , ∆) for all i, 1 ≤ i ≤ q. Since
E1 is a conjunction of elements of At and F1 , . . . , Fq ∈ At, induction yields
that E1 vn−1 Fi is derivable in HC(O, T 0 , ∆) for all i, 1 ≤ i ≤ q. Performing
q − 1 applications of (AndR) thus allows us to derive E1 vn−1 F1 u . . . u Fq in
HC(O, T 0 , ∆). Since T 0 contains the definition E2 ≡ F1 u . . . u Fq , an application
of (DefR) shows that E1 vn E2 is derivable in HC(O, T 0 , ∆).
Second, assume that E1 v` E2 was obtained by an application of (DefL).
Then E1 ∈ Ndef and E2 = F1 u . . . u Fq for elements F1 , . . . , Fq of At. By
our choice of ` we have E1 vgfp,O,T E2 , and thus E1 vgfp,O,T Fi for all i, 1 ≤
i ≤ q. It is sufficient to show, for all i, 1 ≤ i ≤ q, that E1 vn Fi is derivable
in HC(O, T 0 , ∆) since q − 1 applications of (AndR) then yield derivability of
E1 vn E2 in HC(O, T 0 , ∆).
If Fi does not belong to Ndef , then it is an element of Atnv . The definition
of ζ T thus yields Fi ∈ ζET
1
. Consequently, Fi occurs as a conjunct on the right-
hand side of the definition of E1 in T 0 . This implies E1 vgfp,O,T 0 Fi , and thus
E1 vn Fi is derivable in HC(O, T 0 , ∆).
If Fi ∈ Ndef , then E1 vgfp,O,T Fi implies that ζFTi ⊆ ζE
T
1
. Consequently, every
conjunct on the right-hand side of the definition of Fi in T 0 is also a conjunct on
the right-hand side of the definition of E1 in T 0 . This implies E1 vgfp,O,T 0 Fi ,
and thus E1 vn Fi is derivable in HC(O, T 0 , ∆). t
u
This finishes the proof of Proposition 8, and thus shows that hybrid EL-
unification w.r.t. arbitrary EL-ontologies is in NP. NP-hardness does not follow
directly from NP-hardness of classical EL-unification. In fact, as we have seen in
Example 6, an EL-unification problem that does not have a classical unifier may
well have a hybrid unifier. Instead, we reduce EL-matching modulo equivalence
to hybrid EL-unification.
Using the notions introduced in this paper, EL-matching modulo equivalence
can be defined as follows. An EL-matching problem modulo equivalence is an EL-
unification problem of the form {C v D, D v C} such that D does not contain
elements of Ndef . A matcher of such a problem is a classical unifier of it. As
shown in [11], testing whether a matching problem modulo equivalence has a
matcher or not is an NP-complete problem. Thus, NP-hardness of hybrid EL-
unification w.r.t. EL-ontologies is an immediate consequence of the following
lemma, whose (non-trivial) proof can be found in [5].
Lemma 10. If an EL-matching problem modulo equivalence has a hybrid unifier
w.r.t. the empty ontology, then it also has a matcher.
To sum up, we have thus determine the exact worst-case complexity of hybrid
EL-unification.
Theorem 11. The problem of testing whether an EL-unification problem w.r.t.
an arbitrary EL-ontology has a hybrid unifier or not is NP-complete.
5 Conclusions
In this paper, we have proved that hybrid EL-unification w.r.t. arbitrary EL-
ontologies is in NP. The proof of NP-hardness of this problem as well as a more
practical goal-oriented algorithm for hybrid EL-unification that is better than
the brute-force “guess and then test” algorithm sketched above can be found in
[5]. As illustrated by Example 6, computing hybrid unifiers rather than classical
ones may be appropriate in some situations. Nevertheless, the decidability and
complexity of classical EL-unification w.r.t. arbitrary EL-ontologies is an im-
portant topic for future research. We hope that hybrid unification may also be
helpful in this context. Basically, given a hybrid unifier T of Γ w.r.t. O, we can
try to obtain a classical unifier of Γ w.r.t. O by finding an acyclic TBox S such
that O ∪ S entails all the GCIs that (O, T ) entails w.r.t. hybrid semantics, i.e.
C vgfp,O,T D implies C vO∪S D for all (relevant) concept descriptions C, D.
References
1. Baader, F.: Terminological cycles in a description logic with existential restrictions.
In: Gottlob, G., Walsh, T. (eds.) Proc. of the 18th Int. Joint Conf. on Artificial
Intelligence (IJCAI 2003). pp. 325–330. Morgan Kaufmann, Los Altos, Acapulco,
Mexico (2003)
2. Baader, F., Borgwardt, S., Morawska, B.: Unification in the description logic EL
w.r.t. cycle-restricted TBoxes. LTCS-Report 11-05, Chair for Automata Theory,
Institute for Theoretical Computer Science, Technische Universität Dresden, Dres-
den, Germany (2011), see http://lat.inf.tu-dresden.de/research/reports.html.
3. Baader, F., Borgwardt, S., Morawska, B.: Extending unification in EL towards
general TBoxes. In: Proc. of the 13th Int. Conf. on Principles of Knowledge Rep-
resentation and Reasoning (KR 2012). pp. 568–572. AAAI Press/The MIT Press
(2012)
4. Baader, F., Borgwardt, S., Morawska, B.: A goal-oriented algorithm for unification
in ELHR+ w.r.t. cycle-restricted ontologies. In: Thielscher, M., Zhang, D. (eds.)
Pro. of 25th Australasian Joint Conf. on Artificial Intelligence (AI’12). Lecture
Notes in Artificial Intelligence, vol. 7691, pp. 493–504. Springer-Verlag (2012)
5. Baader, F., Fernández Gil, O., Morawska, B.: Hybrid unification in the description
logic EL. LTCS-Report 13-07, Chair for Automata Theory, Institute for Theoretical
Computer Science, Technische Universität Dresden, Dresden, Germany (2013), see
http://lat.inf.tu-dresden.de/research/reports.html.
6. Baader, F., Morawska, B.: Unification in the description logic EL. In: Treinen, R.
(ed.) Proc. of the 20th Int. Conf. on Rewriting Techniques and Applications (RTA
2009). Lecture Notes in Computer Science, vol. 5595, pp. 350–364. Springer-Verlag
(2009)
7. Baader, F., Morawska, B.: Unification in the description logic EL. Logical Methods
in Computer Science 6(3) (2010)
8. Baader, F., Narendran, P.: Unification of concept terms in description logics. J. of
Symbolic Computation 31(3), 277–305 (2001)
9. Brandt, S.: Polynomial time reasoning in a description logic with existential re-
strictions, GCI axioms, and—what else? In: de Mántaras, R.L., Saitta, L. (eds.)
Proc. of the 16th Eur. Conf. on Artificial Intelligence (ECAI 2004). pp. 298–302
(2004)
10. Brandt, S., Model, J.: Subsumption in EL w.r.t. hybrid tboxes. In: Proc. of the
28th German Annual Conf. on Artificial Intelligence (KI’05). pp. 34–48. Lecture
Notes in Artificial Intelligence, Springer-Verlag (2005)
11. Küsters, R.: Non-standard Inferences in Description Logics, Lecture Notes in Ar-
tificial Intelligence, vol. 2100. Springer-Verlag (2001)
12. Novakovic, N.: A proof-theoretic approach to deciding subsumption and comput-
ing least common subsumer in w.r.t. hybrid TBoxes. In: Hölldobler, S., Lutz, C.,
Wansing, H. (eds.) Proc. of the 11th Eur. Conf. on Logics in Artificial Intelli-
gence (JELIA’2004). Lecture Notes in Computer Science, vol. 5293, pp. 311–323.
Springer-Verlag (2008)