=Paper=
{{Paper
|id=Vol-477/paper-33
|storemode=property
|title=Unification in the Description Logic EL
|pdfUrl=https://ceur-ws.org/Vol-477/paper_54.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/BaaderM09
}}
==Unification in the Description Logic EL==
https://ceur-ws.org/Vol-477/paper_54.pdf
Unification in the Description Logic EL
Franz Baader and Barbara Morawska?
Theoretical Computer Science, TU Dresden, Germany
{baader,morawska}@tcs.inf.tu-dresden.de
Abstract. The Description Logic EL has recently drawn considerable
attention since, on the one hand, important inference problems such as
the subsumption problem are polynomial. On the other hand, EL is used
to define large biomedical ontologies. Unification in Description Logics
has been proposed as a novel inference service that can, for example,
be used to detect redundancies in ontologies. The main result of this
paper is that unification in EL is decidable. More precisely, we show
that EL-unification is NP-complete, and thus has the same complexity
as EL-matching.
1 Introduction
Unification in Description Logics was first considered in [7] for the DL FL0 ,
which has the concept constructors conjunction (u), value restriction (∀r.C),
and the top concept (>). It was shown that unification in FL0 is decidable
and ExpTime-complete. The motivation for considering unification in DLs was
to detect redundancies in DL-based ontologies. For example, assume that one
knowledge engineer has defined the concept of all women having only daughters
by the concept term Womanu∀child.Woman. A second knowledge engineer might
represent this notion in a somewhat more fine-grained way, e.g., by using the term
Female u Human in place of Woman. The concept terms Woman u ∀child.Woman
and Female u Human u ∀child.(Female u Human) are not equivalent, but they are
meant to represent the same concept. The two terms can obviously be made
equivalent by substituting the concept name Woman in the first term by the
concept term Female u Human. Of course, it is not necessarily the case that
concept terms that are unifiable in this sense are meant to represent the same
notion. A unifiability test can, however, suggest to the knowledge engineer possi-
ble candidate terms. Unification has, however, not been used in practice as a way
of detecting redundancies. The reason is probably that the only DL for which
a unification algorithm was known was the inexpressive DL FL0 . Unification
in this DL is already of a rather high complexity, and there are no interesting
ontologies that are actually formulated in FL0 .
In this paper, we consider unification in the DL EL. In contrast to the situa-
tion for FL0 , EL is used (in spite of its limited expressive power) in applications,
e.g., to define biomedical ontologies: the large medical ontology Snomed ct1 and
?
A longer version of this paper has been accepted for publication at the 20th Inter-
national Conference on Rewriting Techniques and Applications (RTA 2009) [6].
1
http://www.ihtsdo.org/snomed-ct/
the Gene Ontology2 can be expressed in EL, and the same is true for large parts
of the medical ontology Galen [14]. The second advantage of EL over FL0
is that the subsumption problem remains polynomial in the presence of vari-
ous forms of terminological axioms [1, 2]. The importance of EL can also be seen
from the fact that the new OWL 2 standard3 contains the sub-profile OWL 2 EL,
which is based on (an extension of) EL.
Unification in EL has, to the best of our knowledge, not been investigated
before, but matching (where one side of the equation(s) to be solved does not
contain variables) has been considered in [4, 13]. In particular, it was shown in
[13] that the decision problem, i.e., the problem of deciding whether a given EL-
matching problem has a matcher or not, is NP-complete. Interestingly, FL0 be-
haves better w.r.t. matching than EL: for FL0 , the decision problem is tractable
[5]. In this paper, we show that w.r.t. unification, EL behaves much better than
FL0 : EL-unification is NP-complete, and thus has the same complexity as EL-
matching.
Regarding related work, one also needs to look at results from modal logics.
In fact, it is well-known that there is a close connection between modal logics and
DLs [3]. For example, the DL ALC, which can be obtained by adding negation
to EL or FL0 , corresponds to the basic (multi-)modal logic K. Decidability of
unification in K is a long-standing open problem. Recently, undecidability of
unification in some extensions of K (for example, by the universal modality)
was shown in [15]. The undecidability results in [15] also imply undecidability
of unification in some expressive DLs (e.g., SHIQ). In [11], positive results for
unification in the modal logics K4 and S4 are shown. Unification in sub-Boolean
modal logics (i.e., modal logics that are not closed under all Boolean operations,
such as the modal logic equivalent of EL) has, to the best of our knowledge, not
been considered in the modal logic literature.
In the next section, we define the DL EL and unification in EL more formally.
In Section 3, we recall the characterisation of subsumption and equivalence in
EL from [13]. In Section 4, we show the main result of the paper: unification in
EL is NP-complete.
More information about Description Logics can be found in [3], and about
unification theory in [10].
2 Unification in EL
First, we define the syntax and semantics of EL-concept terms as well as the
subsumption and the equivalence relation on these terms.
Starting with a set Ncon of concept names and a set Nrole of role names,
EL-concept terms are built using the concept constructors top concept (>),
conjunction (u), and existential restriction (∃r.C). The semantics of EL is defined
in the usual way, using the notion of an interpretation I = (DI , ·I ), which
consists of a nonempty domain DI and an interpretation function ·I that assigns
2
http://www.geneontology.org/
3
See http://www.w3.org/TR/owl2-profiles/
Name Syntax Semantics
concept name A AI ⊆ DI
I
role name r r ⊆ D I × DI
top-concept > >I = DI
conjunction C uD (C u D)I = C I ∩ DI
existential restriction ∃r.C (∃r.C)I = {x | ∃y : (x, y) ∈ rI ∧ y ∈ C I }
subsumption CvD C I ⊆ DI
equivalence C≡D C I = DI
Table 1. Syntax and semantics of EL
binary relations on DI to role names and subsets of DI to concept terms, as
shown in the semantics column of Table 1.
The concept term C is subsumed by the concept term D (written C v D)
iff C I ⊆ DI holds for all interpretations I. We say that C is equivalent to
D (written C ≡ D) iff C v D and D v C, i.e., iff C I = DI holds for all
interpretations I. The concept term C is strictly subsumed by the concept term
D (written C @ D) iff C v D and C 6≡ D.
.
A concept definition is of the form A = C where A is a concept name and
C is a concept term. A TBox T is a finite set of concept definitions such that
no concept name occurs more than once on the left-hand side of a concept
definition in T . The TBox T is called acyclic if there are no cyclic dependencies
between its concept definitions. The interpretation I is a model of the TBox
.
T iff AI = C I holds for all concept definitions A = C in T . Subsumption
and equivalence w.r.t. a TBox are defined as follows: C vT D (C ≡T D) iff
C I ⊆ DI (C I = DI ) holds for all models I of T . Subsumption and equivalence
w.r.t. an acyclic TBox can be reduced to subsumption and equivalence of concept
terms (without TBox) by expanding the concept terms w.r.t. the TBox, i.e., by
replacing defined concepts (i.e., concept names occurring on the left-hand side of
a definition) by their definitions (i.e., the corresponding right-hand sides) until
all defined concepts have been replaced. This expansion process may, however,
result in an exponential blow-up [8].
In order to define unification of concept terms, we first introduce the notion
of a substitution operating on concept terms. To this purpose, we partition
the set of concepts names into a set Nv of concept variables (which may be
replaced by substitutions) and a set Nc of concept constants (which must not
be replaced by substitutions). Intuitively, Nv are the concept names that have
possibly been given another name or been specified in more detail in another
concept term describing the same notion. The elements of Nc are the ones of
which it is assumed that the same name is used by all knowledge engineers (e.g.,
standardised names in a certain domain).
A substitution σ is a mapping from Nv into the set of all EL-concept terms.
This mapping is extended to concept terms in the obvious way, i.e.,
– σ(A) := A for all A ∈ Nc ,
– σ(>) := >,
– σ(C u D) := σ(C) u σ(D), and
– σ(∃r.C) := ∃r.σ(C).
Definition 1. An EL-unification problem is of the form Γ = {C1 ≡? D1 , . . . ,
Cn ≡? Dn }, where C1 , D1 , . . . Cn , Dn are EL-concept terms. The substitution σ
is a unifier (or solution) of Γ iff σ(Ci ) ≡ σ(Di ) for i = 1, . . . , n. In this case, Γ
is called solvable or unifiable.
When we say that EL-unification is decidable (NP-complete), then we mean
that the following decision problem is decidable (NP-complete): given an EL-
unification problem Γ , decide whether Γ is solvable or not.
3 Equivalence and subsumption in EL
In order to characterise equivalence of EL-concept terms, the notion of a reduced
EL-concept term is introduced in [13]. A given EL-concept term can be trans-
formed into an equivalent reduced term by applying the following rules modulo
associativity and commutativity of conjunction:
C u>→C for all EL-concept terms C
AuA→A for all concept names A ∈ Ncon
∃r.C u ∃r.D → ∃r.C for all EL-concept terms C, D with C v D
Obviously, these rules are equivalence preserving. We say that the EL-concept
term C is reduced if none of the above rules is applicable to it (modulo asso-
ciativity and commutativity of u). The EL-concept term D is a reduced form
of C if D is reduced and can be obtained from C by applying the above rules
(modulo associativity and commutativity of u). The following theorem is an easy
consequence of Theorem 6.3.1 on page 181 of [13].
Theorem 1. Let C, D be EL-concept terms, and C, b Db reduced forms of C, D,
respectively. Then C ≡ D iff C is identical to D up to associativity and commu-
b b
tativity of u.
This theorem can also be used to derive a recursive characterisation of sub-
sumption in EL. In fact, if C v D, then C u D ≡ C, and thus C and C u D have
the same reduced form. Thus, during reduction, all concept names and existen-
tial restrictions of D must be “eaten up” by corresponding concept names and
existential restrictions of C.
Corollary 1. Let C = A1 u . . . u Ak u ∃r1 .C1 u . . . u ∃rm .Cm and D = B1 u
. . .uB` u∃s1 .D1 u. . .u∃sn .Dn , where A1 , . . . , Ak , B1 , . . . , B` are concept names.
Then C v D iff {B1 , . . . , B` } ⊆ {A1 , . . . , Ak } and for every j, 1 ≤ j ≤ n, there
exists an i, 1 ≤ i ≤ m, such that ri = sj and Ci v Dj .
Note that this corollary also covers the cases where some of the numbers
k, `, m, n are zero. The empty conjunction should then be read as >. The follow-
ing lemma is an immediate consequence of this corollary.
Lemma 1. If C, D are reduced EL-concept terms such that ∃r.D v C, then C
is either >, or of the form C = ∃r.C1 u . . . u ∃r.Cn where n ≥ 1; C1 , . . . , Cn are
reduced and pairwise incomparable w.r.t. subsumption; and D v C1 , . . . , D v Cn .
Conversely, if C, D are EL-concept terms such that C = ∃r.C1 u . . . u ∃r.Cn and
D v C1 , . . . , D v Cn , then ∃r.D v C.
Proof. We have ∃r.D v C iff C u ∃r.D ≡ ∃r.D. Since ∃r.D is reduced, any re-
duced form of C u∃r.D must be identical (up to associativity and commutativity
of u) to ∃r.D. If C 6= >, then the only rule that can be applied to reduce C u∃r.D
is the third one. It is easy to see that we can only obtain ∃r.D by applying this
rule if C is of the form C = ∃r.C1 u . . . u ∃r.Cn where D v C1 , . . . , D v Cn .
Since C was assumed to be reduced, the terms C1 , . . . , Cn must also be reduced
and pairwise incomparable w.r.t. subsumption. t
u
In the proof of decidability of EL-unification, we will make use of the fact
that the inverse strict subsumption order is well-founded.
Proposition 1. There is no infinite sequence C0 , C1 , C2 , C3 , . . . of EL-concept
terms such that C0 @ C1 @ C2 @ C3 @ · · · .
Proof. We define the role depth of an EL-concept term C as the maximal nesting
of existential restrictions in C. Let n0 be the role depth of C0 . Since C0 v Ci
for i ≥ 1, it is an easy consequence of Corollary 1 that the role depth of Ci is
bounded by n0 , and that Ci contains only concept and role names occurring in
C0 . In addition, it is known that, for a given natural number n0 and finite sets
of concept names C and role names R, there are, up to equivalence, only finitely
many EL-concept term built using concept names from C and role names from
R and of a role depth bounded by n0 [9]. Consequently, there are indices i < j
such that Ci ≡ Cj . This contradicts our assumption that Ci @ Cj . t
u
4 The complexity of EL-unification
Before we can describe our decision procedure for EL-unification, we must in-
troduce some notation. An EL-concept term is called an atom iff it is a concept
name (i.e., concept constant or concept variable) or an existential restriction
∃r.D. Obviously, any EL-concept term is (equivalent to) a conjunction of atoms,
where the empty conjunction is >. The set At(C) of atoms of an EL-concept
term C is defined inductively: if C = >, then At(C) := ∅; if C is a concept name,
then At(C) := {C}; if C = ∃r.D then At(C) := {C} ∪ At(D); if C = C1 u C2 ,
then At(C) := At(C1 ) ∪ At(C2 ).
Concept names and existential restrictions ∃r.D where D is a concept name
or > are called flat atoms. The EL-unification problem Γ is flat iff it only contains
equations of the following form:
– X ≡? C where X is a variable and C is a non-variable flat atom;
– X1 u . . . u Xm ≡? Y1 u . . . u Yn where X1 , . . . , Xm , Y1 , . . . , Yn are variables.
By introducing new concept variables and eliminating >, any EL-unification
problem Γ can be transformed in polynomial time into a flat EL-unification
problem Γ 0 such that Γ is solvable iff Γ 0 is solvable. Thus, we may assume
without loss of generality that our input EL-unification problems are flat. Given
a flat EL-unification problem Γ = {C1 ≡? D1 , . . . , Cn ≡? Dn }, we call the atoms
of C1 , D1 , . . . , Cn , Dn the atoms of Γ .
The unifier σ of Γ is called reduced (ground ) iff, for all concept variables
X occurring in Γ , the EL-concept term σ(X) is reduced (does not contain vari-
ables). Obviously, Γ is solvable iff it has a reduced ground unifier. Given a ground
unifier σ of Γ , we consider the set At(σ) of all atoms of σ(X), where X ranges
over all variables occurring in Γ . We call the elements of At(σ) the atoms of σ.
Given EL-concept terms C, D, we define C >is D iff C @ D. Proposition 1
says that the strict order >is defined this way is well-founded. This order is
monotone in the following sense.
Lemma 2. Let C, D, D0 be EL-concept terms such that D >is D0 and C is
reduced and contains at least one occurrence of D. If C 0 is obtained from C by
replacing all occurrences of D by D0 , then C >is C 0 .
Proof. We prove the lemma by induction on the size of C. If C = D, then
C 0 = D0 , and thus C = D >is D0 = C 0 . Thus, assume that C 6= D. In this
case, C obviously cannot be a concept name. If C = ∃r.C1 , then D occurs in
C1 . By induction, we can assume that C1 >is C10 , where C10 is obtained from
C1 by replacing all occurrences of D by D0 . Thus, we have C = ∃r.C1 >is
∃r.C10 = C 0 by Corollary 1. Finally, assume that C = C1 u . . . u Cn for n >
1 atoms C1 , . . . , Cn . Since C is reduced, these atoms are incomparable w.r.t.
subsumption, and since D occurs in C we can assume without loss of generality
that D occurs in C1 . Let C10 , . . . , Cn0 be respectively obtained from C1 , . . . , Cn
by replacing every occurrence of D by D0 , and then reducing the concept term
obtained this way. By induction, we have C1 >is C10 . Assume that C 6>is C 0 .
Since the concept constructors of EL are monotone w.r.t. subsumption v, we
have C v C 0 , and thus C 6>is C 0 means that C ≡ C 0 . Consequently, C =
C1 u . . . u Cn and the reduced form of C10 u . . . u Cn0 must be equal up to
associativity and commutativity of u. If C10 u . . . u Cn0 is not reduced, then
its reduced form is actually a conjunction of m < n atoms, which contradicts
C ≡ C 0 . If C10 u . . . u Cn0 is reduced, then C1 >is C10 implies that there is an i 6= 1
such that Ci ≡ C10 . However, then Ci ≡ C10 A C1 contradicts the fact that the
atoms C1 , . . . , Cn are incomparable w.r.t. subsumption. t
u
We use the order >is on EL-concept terms to define a well-founded order
on ground unifiers. Since >is is well-founded, its multiset extension >m is also
well-founded. Given a ground unifier σ of Γ , we consider the multiset S(σ) of
all EL-concept terms σ(X), where X ranges over all concept variables occurring
in Γ . For two ground unifiers σ, θ of Γ , we define σ θ iff S(σ) >m S(θ). The
ground unifier σ of Γ is minimal iff there is no ground unifier θ of Γ such that
σ θ. The following proposition is an easy consequence of the fact that is
well-founded.
Proposition 2. Let Γ be an EL-unification problem. Then Γ is solvable iff it
has a minimal reduced ground unifier.
In the following, we show that minimal reduced ground unifiers of flat EL-
unification problems satisfy properties that make it easy to check (with an NP-
algorithm) whether such a unifier exists or not.
Lemma 3. Let Γ be a flat EL-unification problem and γ a minimal reduced
ground unifier of Γ . If C is an atom of γ, then there is a non-variable atom D
of Γ such that C ≡ γ(D).
Proof. Since γ is ground, C is either a concept constant or an existential re-
striction. First, assume that C = A for a concept constant A, but there is no
non-variable atom D of Γ such that A ≡ γ(D). This simply means that A does
not occur in Γ . Let γ 0 be the substitution obtained from γ by replacing every
occurrence of A by >. Since equivalence in EL is preserved under replacing con-
cept names by >, and since A does not occur in Γ , it is easy to see that γ 0 is
also a unifier of Γ . However, since γ γ 0 , this contradicts our assumption that
γ is minimal.
Second, assume that C = ∃r.C1 , but there is no non-variable atom D of Γ
such that C ≡ γ(D). We assume that C is maximal (w.r.t. subsumption) with
this property, i.e., for every atom C 0 of γ with C @ C 0 , there is a non-variable
atom D0 of Γ such that C 0 ≡ γ(D0 ). Let D1 , . . . , Dn be all the atoms of Γ
with C v γ(Di ) (i = 1, . . . , n). By our assumptions on C, we actually have
C @ γ(Di ) and, by Lemma 1, the atom Di is also an existential restriction
Di = ∃r.Di0 (i = 1, . . . , n). The conjunction Db := γ(D1 ) u . . . u γ(Dn ) obviously
subsumes C. We claim that this subsumption relationship is actually strict. In
fact, if n = 0, then D b = >, and since C is an atom, it is not equivalent to
>. If n ≥ 1, then C = ∃r.C1 w ∃r.γ(D10 ) u . . . u ∃r.γ(Dn ) would imply (by
Corollary 1) that there is an i, 1 ≤ i ≤ n, with C1 w γ(Di0 ). However, this would
yield C = ∃r.C1 w ∃r.γ(Di0 ) = γ(Di ), which contradicts the fact that C @ γ(Di ).
Thus, we have shown that C @ D. b The substitution γ 0 is obtained from γ by
replacing every occurrence of C by D. b Lemma 2 implies that γ γ 0 . Thus, to
obtain the desired contradiction, it is sufficient to show that γ 0 is a unifier of Γ .
First, consider an equation of the form X ≡? E in Γ , where X is a variable
and E is a non-variable flat atom. If E is a concept constant, then γ(X) = E, and
thus γ 0 (X) = γ(X), which shows that γ 0 solves this equation. Thus, assume that
E = ∃r.E 0 . Since γ is reduced, we actually have γ(X) = ∃r.γ(E 0 ). If C occurs in
γ(E 0 ), then each replacement of C by D b in γ(E 0 ) is matched by the corresponding
replacement in γ(X). Thus, in this case γ 0 again solves the equation. Finally,
assume that C = γ(X). But then C ≡ γ(E) for a non-variable atom E of Γ ,
which contradicts our assumption on C.
Second, consider an equation of the form X1 u. . .uXm ≡? Y1 u. . .uYn where
X1 , . . . , Xm , Y1 , . . . , Yn are variables. Then L := γ(X1 u. . .uXm ) and R := γ(Y1 u
. . .uYn ) reduce to the same reduced EL-concept term J. Let L0 , R0 , J 0 be the EL-
concept terms respectively obtained from L, R, J by replacing every occurrence
of C by D. b We prove that L0 = γ 0 (X1 u . . . u Xm ) and R0 = γ 0 (Y1 u . . . u Yn ) both
reduce to J 0 , which shows that γ 0 solves this equation. It is enough to show that
the reductions are invariant under the replacement of C by D. b Obviously, all the
interesting reductions are of the form E1 u E2 → E1 where E1 , E2 are existential
restrictions such that E1 v E2 . Since γ is reduced, we can assume that E1 , E2
are reduced. Let E10 , E20 be respectively obtained from E1 , E2 by replacing every
occurrence of C by D. b We must show that E 0 u E 0 reduces to E 0 . For this,
1 2 1
it is enough to show that E10 v E20 . Assume that an occurrence of C in E1 is
actually needed to have the subsumption E1 v E2 . Then there is an existential
restriction C 0 in E2 such that C v C 0 . If C = C 0 , then both are replaced by D, b
0 0
and thus this replacement is harmless. Otherwise, C @ C . Since C is an atom
of γ, maximality of C yields that there is a non-variable atom D0 of Γ such that
C 0 ≡ γ(D0 ). Now C @ C 0 ≡ γ(D0 ) implies that there is an i, 1 ≤ i ≤ n, such
that D0 = Di . Thus, C 0 is actually one of the conjuncts of D, b which again shows
that replacing C by D b is harmless. Thus, we have shown that E 0 v E 0 , which
1 2
completes the proof of the lemma. t
u
The next proposition is an easy consequence of this lemma.
Proposition 3. Let Γ be a flat EL-unification problem and γ a minimal reduced
ground unifier of Γ . If X is a concept variable occurring in Γ , then γ(X) ≡ >
or there are non-variable atoms D1 , . . . , Dn (n ≥ 1) of Γ such that γ(X) ≡
γ(D1 ) u . . . u γ(Dn ).
Proof. If γ(X) 6≡ >, then it is a non-empty conjunction of atoms, i.e., there are
atoms C1 , . . . , Cn (n ≥ 1) such that γ(X) = C1 u . . . u Cn . Then C1 , . . . , Cn are
atoms of γ, and thus Lemma 3 yields non-variable atoms D1 , . . . , Dn of Γ such
that Ci ≡ γ(Di ) for i = 1, . . . n. Consequently, γ(X) ≡ γ(D1 ) u . . . u γ(Dn ). t u
This proposition suggests the following non-deterministic algorithm for de-
ciding solvability of a given flat EL-unification problem Γ :
1. For every variable X occurring in Γ , guess a finite, possibly empty, set SX
of non-variable atoms of Γ .
2. We say that the variable X directly depends on the variable Y if Y occurs
in an atom of SX . Let depends on be the transitive closure of directly de-
pends on. If there is a variable that depends on itself, then the algorithm
returns “fail.” Otherwise, there exists a strict linear order > on the variables
occurring in Γ such that X > Y if X depends on Y .
3. We define the substitution σ along the linear order >:
– If X is the least variable w.r.t. >, then SX does not contain any variables.
We define σ(X) to be the conjunction of the elements of SX , where the
empty conjunction is >.
– Assume that σ(Y ) is defined for all variables Y < X. Then SX only
contains variables Y for which σ(Y ) is already defined. If SX is empty,
then we define σ(X) := >. Otherwise, let SX = {D1 , . . . , Dn }. We define
σ(X) := σ(D1 ) u . . . u σ(Dn ).
4. Test whether the substitution σ computed in the previous step is a unifier
of Γ . If this is the case, then return σ; otherwise, return “fail.”
This algorithm is trivially sound since it only returns substitutions that are
unifiers of Γ . In addition, it obviously always terminates. Thus, to show correct-
ness of our algorithm, it is sufficient to show that it is complete.
Lemma 4 (completeness). If Γ is solvable, then there is a way of guessing
in Step 1 subsets SX of the non-variable atoms of Γ such that the depends on
relation determined in Step 2 is acyclic and the substitution σ computed in Step 3
is a unifier of Γ .
Proof. If Γ is solvable, then it has a minimal reduced ground unifier γ. By
Proposition 3, for every variable X occurring in Γ we have γ(X) ≡ > or there
are non-variable atoms D1 , . . . , Dn (n ≥ 1) of Γ such that γ(X) ≡ γ(D1 ) u
. . . u γ(Dn ). If γ(X) ≡ >, then we define SX := ∅. Otherwise, we define SX :=
{D1 , . . . , Dn }.
We show that the relation depends on induced by these sets SX is acyclic, i.e.,
there is no variable X such that X depends on itself. If X directly depends on Y ,
then Y occurs in an element of SX . Since SX consists of non-variable atoms of
the flat unification problem Γ , this means that there is a role name r such that
∃r.Y ∈ SX . Consequently, we have γ(X) v ∃r.γ(Y ). Thus, if X depends on X,
then there are k ≥ 1 role names r1 , . . . , rk such that γ(X) v ∃r1 . · · · ∃rk .γ(X).
This is clearly not possible since γ(X) cannot be subsumed by an EL-concept
term whose role depth is larger than the role depth of γ(X).
To show that the substitution σ induced by the sets SX is a unifier of Γ ,
we prove that σ is equivalent to γ, i.e., σ(X) ≡ γ(X) holds for all variables X
occurring in Γ . The substitution σ is defined along the linear order >. If X is the
least variable w.r.t. >, then SX does not contain any variables. If SX is empty,
then σ(X) = > ≡ γ(X). Otherwise, let SX = {D1 , . . . , Dn }. Since the atoms Di
do not contain variables, we have Di = γ(Di ). Thus, the definitions of SX and
of σ yield σ(X) = D1 u . . . u Dn = γ(D1 ) u . . . u γ(Dn ) ≡ γ(X).
Assume that σ(Y ) ≡ γ(Y ) holds for all variables Y < X. If SX = ∅, then
we have again σ(X) = > ≡ γ(X). Otherwise, let SX = {D1 , . . . , Dn }. Since the
atoms Di contain only variables that are smaller than X, we have σ(Di ) ≡ γ(Di )
by induction. Thus, the definitions of SX and of σ yield σ(X) = σ(D1 ) u . . . u
σ(Dn ) ≡ γ(D1 ) u . . . u γ(Dn ) ≡ γ(X). t
u
Note that our proof of completeness actually shows that, up to equivalence,
the algorithm returns all minimal reduced ground unifiers of Γ .
Theorem 2. EL-unification is NP-complete.
Proof. NP-hardness follows from the fact that EL-matching is NP-complete [13].
To show that the problem can be decided by a non-deterministic polynomial-
time algorithm, we analyse the complexity of our algorithm. Obviously, guessing
the sets SX (Step 1) can be done within NP. Computing the depends on relation
and checking it for acyclicity (Step 2) is clearly polynomial.
Steps 3 and 4 are more problematic. In fact, since a variable may occur in
different atoms of Γ , the substitution σ computed in Step 3 may be of exponential
size. This is actually the same reason that makes a naive algorithm for syntactic
unification compute an exponentially large most general unifier [10]. As in the
case of syntactic unification, the solution to this problem is basically structure
sharing. Instead of computing the substitution σ explicitly, we view its definition
as an acyclic TBox. To be more precise, for every concept variable X occurring
.
in Γ , the TBox Tσ contains the concept definition X = > if SX = ∅ and
.
X = D1 u . . . u Dn if SX = {D1 , . . . , Dn } (n ≥ 1). Instead of computing σ in
Step 3, we compute Tσ . Because of the acyclicity test in Step 2, we know that
Tσ is an acyclic TBox. The size of Tσ is obviously polynomial in the size of Γ ,
and thus this modified Step 3 is polynomial. It is easy to see that applying the
substitution σ is the same as expanding the concept terms C, D w.r.t. the TBox
Tσ . This implies that, for every equation C ≡? D in Γ , we have C ≡Tσ D iff
σ(C) ≡ σ(D). Thus, testing whether σ is a unifier of Γ can be reduced to testing
whether C ≡Tσ D holds for every equation C ≡? D in Γ . Since subsumption
(and thus equivalence) in EL w.r.t. acyclic TBoxes can be decided in polynomial
time [1],4 this completes the proof of the theorem. t
u
5 Conclusion
In this paper, we have shown that unification in the DL EL is NP-complete.
There are interesting differences between the behaviour of EL and the closely
related DL FL0 w.r.t. unification and matching. Unification in FL0 is ExpTime-
complete, and thus considerably harder than EL-unification. In contrast, FL0 -
matching is polynomial, and thus considerably easier than EL-matching, which
is NP-complete.
There are several interesting directions for future research. On the one hand,
the NP-algorithm for unification in EL presented above is a typical “guess and
then test” NP-algorithm, and thus it is unlikely that a direct implementation
of this algorithm will perform well in practice. In an optimized implementation
one needs to interleave the guessing with the testing phase such that unsuccess-
ful branches in the search tree can be detected as early as possible. Regarding
extensions of the theoretical result, we will on the one hand consider tractable
extensions of EL that are relevant for medical ontologies (e.g., by the bottom
concept, by reflexive and transitive roles). On the other hand, we will consider
unification in EL w.r.t. general concept inclusion axioms (GCIs).
4
Of course, the polynomial-time subsumption algorithm does not expand the TBox.
References
1. F. Baader. Terminological cycles in a description logic with existential restrictions.
In Proc. IJCAI’03, 2003.
2. F. Baader, S. Brandt, and C. Lutz. Pushing the EL envelope. In Proc. IJCAI’05,
2005.
3. F. Baader, D. Calvanese, D. McGuinness, D. Nardi, and P. F. Patel-Schneider, edi-
tors. The Description Logic Handbook: Theory, Implementation, and Applications.
Cambridge University Press, 2003.
4. F. Baader and R. Küsters. Matching in description logics with existential restric-
tions. In Proc. KR’00, 2000.
5. F. Baader, R. Küsters, A. Borgida, and D. L. McGuinness. Matching in description
logics. J. of Logic and Computation, 9(3), 1999.
6. F. Baader, and B. Morawska. Unification in the Description Logic EL. In Proc.
RTA’09, Springer LNCS, 2009. To appear.
7. F. Baader and P. Narendran. Unification of concepts terms in description logics.
J. of Symbolic Computation, 31(3), 2001.
8. F. Baader and W. Nutt. Basic description logics. In [3], 2003.
9. F. Baader, B. Sertkaya, and A.-Y. Turhan. Computing the least common subsumer
w.r.t. a background terminology. J. of Applied Logic, 5(3), 2007.
10. Franz Baader and Wayne Snyder. Unification theory. In Handbook of Automated
Reasoning, volume I. Elsevier Science Publishers, 2001.
11. S. Ghilardi. Best solving modal equations. Ann. Pure Appl. Logic, 102(3), 2000.
12. 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),
2003.
13. R. Küsters. Non-standard Inferences in Description Logics, Sprinfer LNAI 2100,
2001.
14. A. Rector and I. Horrocks. Experience building a large, re-usable medical ontol-
ogy using a description logic with transitivity and concept inclusions. In Proc.
AAAI’97, 1997.
15. F. Wolter and M. Zakharyaschev. Undecidability of the unification and admissi-
bility problems for modal and description logics, ACM Trans. Comput. Log., 9(4),
2008.