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 de ne large biomedical ontologies. Uni cation 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 uni cation in EL is decidable. More precisely, we show that EL-uni cation is NP-complete, and thus has the same complexity as EL-matching.
the Gene Ontology2 can be expressed in E L, and the same is true for large parts
of the medical ontology Galen [
Uni cation in E L 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 [
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 [
In the next section, we de ne the DL E L and uni cation in E L more formally.
In Section 3, we recall the characterisation of subsumption and equivalence in
E L from [
More information about Description Logics can be found in [
First, we de ne the syntax and semantics of E L-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, E L-concept terms are built using the concept constructors top concept (>), conjunction (u), and existential restriction (9r:C). The semantics of E L is de ned 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-pro les/ concept name A AI DI role name r rI DI DI top-concept > >I = DI conjunction C u D (C u D)I = CI \ DI existential restriction 9r:C (9r:C)I = fx j 9y : (x; y) 2 rI ^ y 2 CIg subsumption equivalence
C v D C D
CI DI
CI = DI 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) i CI DI holds for all interpretations I. We say that C is equivalent to D (written C D) i C v D and D v C, i.e., i CI = DI holds for all interpretations I. The concept term C is strictly subsumed by the concept term D (written C @ D) i C v D and C 6 D.
A concept de nition is of the form A =: C where A is a concept name and
C is a concept term. A TBox T is a nite set of concept de nitions such that
no concept name occurs more than once on the left-hand side of a concept
de nition in T . The TBox T is called acyclic if there are no cyclic dependencies
between its concept de nitions. The interpretation I :is a model of the TBox
T i AI = CI holds for all concept de nitions A = C in T . Subsumption
and equivalence w.r.t. a TBox are de ned as follows: C vT D (C T D) i
CI DI (CI = 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 de ned concepts (i.e., concept names occurring on the left-hand side of
a de nition) by their de nitions (i.e., the corresponding right-hand sides) until
all de ned concepts have been replaced. This expansion process may, however,
result in an exponential blow-up [
In order to de ne uni cation of concept terms, we rst 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 speci ed 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 2 Nc, (>) := >, (C u D) := (C) u (9r:C) := 9r: (C).
(D), and De nition 1. An E L-uni cation problem is of the form = fC1 ? D1; : : : ; Cn ? Dng, where C1; D1; : : : Cn; Dn are E L-concept terms. The substitution is a uni er (or solution) of i (Ci) (Di) for i = 1; : : : ; n. In this case, is called solvable or uni able.
When we say that E L-uni cation is decidable (NP-complete), then we mean that the following decision problem is decidable (NP-complete): given an E Luni cation problem , decide whether is solvable or not. 3
In order to characterise equivalence of E L-concept terms, the notion of a reduced
E L-concept term is introduced in [
C u > ! C A u A ! A for all E L-concept terms C for all concept names A 2 Ncon 9r:C u 9r:D ! 9r:C
for all E L-concept terms C; D with C v D
Obviously, these rules are equivalence preserving. We say that the E L-concept
term C is reduced if none of the above rules is applicable to it (modulo
associativity and commutativity of u). The E L-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 [
Theorem 1. Let C; D be E L-concept terms, and Cb; Db reduced forms of C; D, respectively. Then C D i Cb is identical to Db up to associativity and commutativity of u.
This theorem can also be used to derive a recursive characterisation of subsumption in E L. 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 existential 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 9r1:C1 u : : : u 9rm:Cm and D = B1 u : : : u B` u 9s1:D1 u : : : u 9sn:Dn, where A1; : : : ; Ak; B1; : : : ; B` are concept names. Then C v D i fB1; : : : ; B`g fA1; : : : ; Akg 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 following lemma is an immediate consequence of this corollary.
Lemma 1. If C; D are reduced E L-concept terms such that 9r:D v C, then C is either >, or of the form C = 9r:C1 u : : : u 9r: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 E L-concept terms such that C = 9r:C1 u : : : u 9r:Cn and D v C1; : : : ; D v Cn, then 9r:D v C.
Proof. We have 9r:D v C i C u 9r:D 9r:D. Since 9r:D is reduced, any reduced form of C u 9r:D must be identical (up to associativity and commutativity of u) to 9r:D. If C 6= >, then the only rule that can be applied to reduce C u9r:D is the third one. It is easy to see that we can only obtain 9r:D by applying this rule if C is of the form C = 9r:C1 u : : : u 9r: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. tu
In the proof of decidability of E L-uni cation, we will make use of the fact that the inverse strict subsumption order is well-founded.
Proof. We de ne the role depth of an E L-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 nite sets
of concept names C and role names R, there are, up to equivalence, only nitely
many E L-concept term built using concept names from C and role names from
R and of a role depth bounded by n0 [
Before we can describe our decision procedure for E L-uni cation, we must introduce some notation. An E L-concept term is called an atom i it is a concept name (i.e., concept constant or concept variable) or an existential restriction 9r:D. Obviously, any E L-concept term is (equivalent to) a conjunction of atoms, where the empty conjunction is >. The set At (C) of atoms of an E L-concept term C is de ned inductively: if C = >, then At (C) := ;; if C is a concept name, then At (C) := fCg; if C = 9r:D then At (C) := fCg [ At (D); if C = C1 u C2, then At (C) := At (C1) [ At (C2).
Concept names and existential restrictions 9r:D where D is a concept name or > are called at atoms. The E L-uni cation problem is at i it only contains equations of the following form: { X ? C where X is a variable and C is a non-variable at atom; { X1 u : : : u Xm ? Y1 u : : : u Yn where X1; : : : ; Xm; Y1; : : : ; Yn are variables. By introducing new concept variables and eliminating >, any E L-uni cation problem can be transformed in polynomial time into a at E L-uni cation problem 0 such that is solvable i 0 is solvable. Thus, we may assume without loss of generality that our input E L-uni cation problems are at. Given a at E L-uni cation problem = fC1 ? D1; : : : ; Cn ? Dng, we call the atoms of C1; D1; : : : ; Cn; Dn the atoms of .
The uni er of is called reduced (ground ) i , for all concept variables X occurring in , the E L-concept term (X) is reduced (does not contain variables). Obviously, is solvable i it has a reduced ground uni er. Given a ground uni er 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 E L-concept terms C; D, we de ne C >is D i C @ D. Proposition 1 says that the strict order >is de ned this way is well-founded. This order is monotone in the following sense.
Lemma 2. Let C; D; D0 be E L-concept terms such that D >is D0 and C is reduced and contains at least one occurrence of D. If C0 is obtained from C by replacing all occurrences of D by D0, then C >is C0.
Proof. We prove the lemma by induction on the size of C. If C = D, then C0 = D0, and thus C = D >is D0 = C0. Thus, assume that C 6= D. In this case, C obviously cannot be a concept name. If C = 9r: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 = 9r:C1 >is 9r:C10 = C0 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 C0. Since the concept constructors of E L are monotone w.r.t. subsumption v, we have C v C0, and thus C 6>is C0 means that C C0. 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 C0. 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. tu
We use the order >is on E L-concept terms to de ne a well-founded order on ground uni ers. Since >is is well-founded, its multiset extension >m is also well-founded. Given a ground uni er of , we consider the multiset S( ) of all E L-concept terms (X), where X ranges over all concept variables occurring in . For two ground uni ers ; of , we de ne i S( ) >m S( ). The ground uni er of is minimal i there is no ground uni er of such that . The following proposition is an easy consequence of the fact that is well-founded.
has a minimal reduced ground uni er. is solvable i it
In the following, we show that minimal reduced ground uni ers of at E Luni cation problems satisfy properties that make it easy to check (with an NPalgorithm) whether such a uni er exists or not.
Lemma 3. Let be a at E L-uni cation problem and a minimal reduced ground uni er 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 restriction. 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 E L is preserved under replacing concept names by >, and since A does not occur in , it is easy to see that 0 is also a uni er of . However, since 0, this contradicts our assumption that is minimal.
Second, assume that C = 9r: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 C0 of with C @ C0, there is a non-variable atom D0 of such that C0 (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 = 9r: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 Db = >, and since C is an atom, it is not equivalent to >. If n 1, then C = 9r:C1 w 9r: (D10) u : : : u 9r: (Dn) would imply (by Corollary 1) that there is an i; 1 i n, with C1 w (Di0). However, this would yield C = 9r:C1 w 9r: (Di0) = (Di), which contradicts the fact that C @ (Di). Thus, we have shown that C @ Db . The substitution 0 is obtained from by replacing every occurrence of C by Db . Lemma 2 implies that 0. Thus, to obtain the desired contradiction, it is su cient to show that 0 is a uni er of .
First, consider an equation of the form X ? E in , where X is a variable and E is a non-variable at 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 = 9r:E0. Since is reduced, we actually have (X) = 9r: (E0). If C occurs in (E0), then each replacement of C by Db in (E0) 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 : : : u Xm ? Y1 u : : : u Yn where X1; : : : ; Xm; Y1; : : : ; Yn are variables. Then L := (X1u: : :uXm) and R := (Y1u : : :uYn) reduce to the same reduced E L-concept term J . Let L0; R0; J 0 be the E Lconcept terms respectively obtained from L; R; J by replacing every occurrence of C by Db . 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 Db . 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 Db . We must show that E10 u E20 reduces to E10. For this, 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 C0 in E2 such that C v C0. If C = C0, then both are replaced by Db , and thus this replacement is harmless. Otherwise, C @ C0. Since C0 is an atom of , maximality of C yields that there is a non-variable atom D0 of such that C0 (D0). Now C @ C0 (D0) implies that there is an i; 1 i n, such that D0 = Di. Thus, C0 is actually one of the conjuncts of Db , which again shows that replacing C by Db is harmless. Thus, we have shown that E10 v E20, which completes the proof of the lemma. tu
The next proposition is an easy consequence of this lemma.
Proposition 3. Let be a at E L-uni cation problem and ground uni er of . If X is a concept variable occurring in or there are non-variable atoms D1; : : : ; Dn (n 1) of (D1) u : : : u (Dn). a minimal reduced , then (X) > such that (X) 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). tu
This proposition suggests the following non-deterministic algorithm for deciding solvability of a given at E L-uni cation problem : 1. For every variable X occurring in , guess a nite, 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 depends 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 de ne the substitution along the linear order >: { If X is the least variable w.r.t. >, then SX does not contain any variables.
We de ne (X) to be the conjunction of the elements of SX , where the empty conjunction is >. { Assume that (Y ) is de ned for all variables Y < X. Then SX only contains variables Y for which (Y ) is already de ned. If SX is empty, then we de ne (X) := >. Otherwise, let SX = fD1; : : : ; Dng. We de ne (X) := (D1) u : : : u (Dn). 4. Test whether the substitution computed in the previous step is a uni er of . If this is the case, then return ; otherwise, return \fail."
This algorithm is trivially sound since it only returns substitutions that are uni ers of . In addition, it obviously always terminates. Thus, to show correctness of our algorithm, it is su cient 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 uni er of .
Proof. If is solvable, then it has a minimal reduced ground uni er . 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 de ne SX := ;. Otherwise, we de ne SX := fD1; : : : ; Dng.
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 at uni cation problem , this means that there is a role name r such that 9r:Y 2 SX . Consequently, we have (X) v 9r: (Y ). Thus, if X depends on X, then there are k 1 role names r1; : : : ; rk such that (X) v 9r1: 9rk: (X). This is clearly not possible since (X) cannot be subsumed by an E L-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 uni er of , we prove that is equivalent to , i.e., (X) (X) holds for all variables X occurring in . The substitution is de ned 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 = fD1; : : : ; Dng. Since the atoms Di do not contain variables, we have Di = (Di). Thus, the de nitions 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 = fD1; : : : ; Dng. Since the atoms Di contain only variables that are smaller than X, we have (Di) (Di) by induction. Thus, the de nitions of SX and of yield (X) = (D1) u : : : u (Dn) (D1) u : : : u (Dn) (X). tu
Note that our proof of completeness actually shows that, up to equivalence, the algorithm returns all minimal reduced ground uni ers of .
Proof. NP-hardness follows from the fact that E L-matching is NP-complete [
Steps 3 and 4 are more problematic. In fact, since a variable may occur in
di erent 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
uni cation compute an exponentially large most general uni er [
In this paper, we have shown that uni cation in the DL E L is NP-complete. There are interesting di erences between the behaviour of E L and the closely related DL F L0 w.r.t. uni cation and matching. Uni cation in F L0 is ExpTimecomplete, and thus considerably harder than E L-uni cation. In contrast, F L0matching is polynomial, and thus considerably easier than E L-matching, which is NP-complete.
There are several interesting directions for future research. On the one hand, the NP-algorithm for uni cation in E L 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 unsuccessful 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 E L that are relevant for medical ontologies (e.g., by the bottom concept, by re exive and transitive roles). On the other hand, we will consider uni cation in E L w.r.t. general concept inclusion axioms (GCIs). 4 Of course, the polynomial-time subsumption algorithm does not expand the TBox.