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 inexpressive Description Logic EL is of particular interest in this context since, on the one hand, several large biomedical ontologies are de ned using EL. On the other hand, uni cation in EL has recently been shown to be NP-complete, and thus of considerably lower complexity than uni cation in other DLs of similarly restricted expressive power. However, EL allows the use of the top concept (>), which represents the whole interpretation domain, whereas the large medical ontology SNOMED CT makes no use of this feature. Surprisingly, removing the top concept from EL makes the uni cation problem considerably harder. More precisely, we will show that uni cation in EL without the top concept is PSpace-complete.
Uni cation in DLs has been proposed in [
whereas another knowledge engineer represent this notion in a somewhat di erent way, e.g., by using the concept term
These two concept terms are not equivalent, but they are nevertheless meant to represent the same concept. They can obviously be made equivalent by substituting the concept name Professor in the rst term by the concept term Teacher u Researcher and the concept name Woman in the second term by the concept term Person u Female. We call a substitution that makes two concept terms equivalent a uni er of the two terms. Such a uni er proposes de nitions ? Supported by DFG under grant BA 1122/14-1 for the concept names that are used as variables. In our example, we know that, if we de ne Woman as Person u Female and Professor as Teacher u Researcher, then the two concept terms from above are equivalent w.r.t. these de nitions.
In [
However, the large medical ontology SNOMED CT is not formulated in E L, but rather in its sub-logic E L >, which di ers from E L in that the use of the top concept is disallowed. If we employ E L-uni cation to detect redundancies in (extensions of) SNOMED CT, then a uni er may introduce concept terms that contain the top concept, and thus propose de nitions for concept names that are of a form that is not used in SNOMED CT. Apart from this practical motivation for investigating uni cation in E L >, we also found it interesting to see how such a small change in the logic in uences the uni cation problem. Surprisingly, it turned out that the complexity of the problem increases considerably (from NP to PSpace). In addition, compared to E L-uni cation, quite di erent methods had to be developed to actually solve E L >-uni cation problems. In particular, we will show in this paper, that|similar to the case of F L0-uni cation|E L >uni cation can be reduced to solving certain language equations. In contrast to the case of F L0-uni cation, these language equations can be solved in PSpace rather than ExpTime, which we show by a reduction to the emptiness problem for alternating automata on nite words.
Complete proofs of the results presented in this paper can be found in [
>
In this paper, we deal with the description logic E L in which concept terms
are built from concept names (NC ) and role names (NR) using the constructors
conjunction (u), existential restriction (9r:C) and the top concept (>). In the
restricted description logic E L >, concept terms may not contain >. As usual,
these concepts are interpreted as sets over some domain [
An E L-concept term is called an atom i it is a concept name A 2 NC or an existential restriction 9r:D. Concept names and existential restrictions Lemma 1. Let C = A1 u : : : u Ak u 9r1:C1 u : : : u 9rm:Cm and D = B1 u : : : u Bl u9s1:D1 u: : :u9sn:Dn be two E L-concept terms, where A1; : : : ; Ak; B1; : : : ; Bl are concept names. Then C v D i fB1; : : : ; Blg fA1; : : : ; Akg and for every j 2 f1; : : : ; ng there exists an i 2 f1; : : : ; mg such that ri = sj and Ci v Dj . In particular, this means that C v D i for every top-level atom D0 of D there is a top-level atom C0 of C such that C0 v D0.
Modulo equivalence, the subsumption relation is a partial order on concept terms. In E L, the top concept > is the greatest element w.r.t. this order. In E L >, there are many incomparable maximal concept terms. We will see below that these are exactly the E L >-concept terms of the form 9r1: 9rn:A for n 0 role names r1; : : : ; rn and a concept name A. We call such concept terms particles. The set Part(C) of all particles of a given E L >-concept term C is de ned as { Part(C) := fCg if C is a concept name, { Part(C) := f9r:E j E 2 Part(D)g if C = 9r:D, { Part(C) := Part(C1) [ Part(C2) if C = C1 u C2.
For example, the particles of C = A u 9r:(A u 9r:B) are A; 9r:A; 9r:9r:B. Such particles will play an important role in our E L >-uni cation algorithm. The next lemma states that particles are indeed the maximal concept terms w.r.t. to subsumption in E L >, and that the particles subsuming an E L >-concept term C are exactly the particles of C.
Lemma 2. Let C be an E L 1. If B v C, then B C. 2. B 2 Part(C) i C v B.
>-concept term and B a particle. 3
> To de ne uni cation in E L and E L > simultaneously, let L 2 fE L; E L >g. When de ning uni cation in L, we assume that the set of concepts names is partitioned 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). An L-substitution is a mapping from Nv into the set of all L-concept terms. This mapping is extended to concept terms in the usual way, i.e., by replacing all occurrences of variables in the term by their -images. An L-concept term is called ground if it contains no variables, and an L-substitution is called ground if the concept terms (X) are ground for all X 2 Nv.
Uni cation tries to make concept terms equivalent by applying a substitution. De nition 1. An L-uni cation problem is of the form = fC1 ? D1; : : : ; Cn ? Dng, where C1; D1; : : : Cn; Dn are L-concept terms. The L-substitution is an L-uni er of i it solves all the equations Ci ? Di in , i.e., i (Ci) (Di) for i = 1; : : : ; n. In this case, is called L-uni able. In the following, we will use the subsumption C v? D as an abbreviation for the equation C u D ? C. Obviously, solves this equation i (C) v (D).
Clearly, every E L >-uni cation problem is also an E L-uni cation problem. Whether is L-uni able or not may depend, however, on whether L = E L or L = E L >. As an example, consider the problem := fA v? X; B v? Xg, where A; B are distinct concept constants and X is a concept variable. Obviously, the substitution that replaces X by > is an E L-uni er of . However, does not have an E L >-uni er. In fact, for such a uni er , the E L >-concept term (X) would need to satisfy A v (X) and B v (X). Since A and B are particles, Lemma 2 would imply A (X) B and thus A B, which is not the case.
It is easy to see that, for both L = E L and L = E L >, an L-uni cation
problem has an L-uni er i it has a ground L-uni er that uses only concept
and role names occurring in ,3 i.e., for all variables X, the L-concept term (X)
is a ground term that contains only such concept and role names. In addition,
we may without loss of generality restrict our attention to at L-uni cation
problems, i.e., uni cation problems in which the left- and right-hand sides of
equations are at L-concept terms (see, e.g., [
Given a at L-uni cation problem , we denote by At( ) the set of all atoms of , i.e., the union of all sets of atoms of the concept terms occurring in . By Var( ) we denote the variables that occur in , and by NV( ) := At( )nVar( ) the set of all non-variable atoms of .
EL-uni cation by guessing acyclic assignments
The NP-algorithm for E L-uni cation introduced in [
The algorithm then tests whether the substitution S computed this way is a
uni er of . If this is the case, then this run returns S; otherwise, it returns
\fail." In [
As an example, consider the EL >-uni cation problem := fA u B ? Y; B u C
? Z; 9r:Y v? X; 9r:Z v? Xg; where X; Y; Z are concept variables and A; B; C are distinct concept constants. We claim that, up to equivalence, the substitution that maps X to 9r:B, Y to A u B, and Z to B u C is the only EL >-uni er of . In fact, any EL >-uni er of must map Y to A u B and Z to B u C, and thus satisfy 9r:(A u B) v (X) and 9r:(B u C) v (X). Lemma 1 then yields that the only possible top-level atom of (X) is 9r:B. However, there is no non-variable atom D 2 NV( ) such that (D) is equivalent to 9r:B. This shows that has an EL >-uni er, but this uni er cannot be computed by the modi ed algorithm sketched above.
The main idea underlying the EL >-uni cation algorithm introduced in the next section is that one starts with an EL-uni er, and then conjoins \appropriate" particles to the images of the variables that are replaced by > by this uni er. It is, however, not so easy to decide which particles can be added this way without turning the EL-uni er into an EL >-substitution that no longer solves the uni cation problem. 4
In the following, let be a at EL >-uni cation problem. Without loss of generality we assume that consists of subsumptions of the form C1 u : : : u Cn v? D for atoms C1; : : : ; Cn; D. Our decision procedure for EL >-uni ability proceeds in four steps.
Step 1. If S is an acyclic assignment guessed by the EL-uni cation algorithm sketched above, then D 2 S(X) implies that the subsumption S(X) v S(D) holds for the substitution S induced by S. Instead of guessing just subsumptions between variables and non-variable atoms, our E L >-uni cation algorithm starts with guessing subsumptions between arbitrary atoms of . To be more precise, it guesses a mapping : At( )2 ! f0; 1g, which speci es which subsumptions between atoms of should hold for the E L >-uni er that it tries to generate: if (D1; D2) = 1 for D1; D2 2 At( ), then this means that the search for a uni er is restricted (in this branch of the search tree) to substitutions satisfying (D1) v (D2). Obviously, any such mapping also yields an assignment
S (X) := fD 2 NV( ) j (X; D) = 1g; and we require that this assignment is acyclic and induces an E L-uni er of . De nition 2. The mapping : At( )2 ! f0; 1g is called a subsumption mapping for if it satis es the following three conditions: 1. It respects the properties of subsumption in E L: (a) (D; D) = 1 for each D 2 At( ). (b) (A1; A2) = 0 for distinct concept constants A1; A2 2 At( ). (c) (9r:C1; 9s:C2) = 0 for distinct r; s 2 NR with 9r:C1; 9s:C2 2 At( ). (d) (A; 9r:C) = (9r:C; A) = 0 for each constant A 2 At( ), role name r and variable or constant C with 9r:C 2 At( ). (e) If 9r:C1; 9r:C2 2 At( ), then (9r:C1; 9r:C2) = (C1; C2). (f ) For all atoms D1; D2; D3 2 At( ), if (D1; D2) = (D2; D3) = 1, then (D1; D3) = 1. 2. It induces an E L-substitution, i.e., the assignment S is acyclic and thus induces a substitution S , which we will simply denote by . 3. It respects the subsumptions of , i.e., it satis es the following conditions for each subsumption C1 u : : : u Cn v? D in : (a) If D is a non-variable atom, then there is at least one Ci such that (Ci; D) = 1. (b) If D is a variable and (D; C) = 1 for a non-variable atom C 2 NV( ), then there is at least one Ci with (Ci; C) = 1.
Though this is not really necessary for the proof of correctness of our E L >uni cation algorithm, it can be shown that the substitution induced by a subsumption mapping for is indeed an E L-uni er of . It should be noted that need not be an E L >-uni er of . In addition, need not agree with on every subsumption between atoms of . The reason for this is that speci es subsumptions which should hold in the E L >-uni er of to be constructed. To turn into such an E L >-uni er, we may have to add certain particles, and these additions may invalidate subsumptions that hold for . However, we will ensure that no subsumption claimed by is invalidated.
[ Step 2. In this step, we use to turn into a uni cation problem that has only variables on the right-hand sides of subsumptions. More precisely, we de ne ; := , where := fC1 u : : : u Cn v? X 2 j X is a variable of g; := fC v? X j X is a variable and C an atom of with (C; X) = 1g: For an arbitrary E L
>-substitution , we de ne S (X) := fD 2 NV( ) j (X) v (D)g; and write S S if S (X) S (X) for every variable X. The following lemma states the connection between E L >-uni ability of and of ; , using the notation that we have just introduced.
Lemma 3. Let be a at E L ments are equivalent for any E L >-uni cation problem. Then the following state
>-substitution : 1. is an E L >-uni er of . 2. There is a subsumption mapping an E L >-uni er of ; and S : At( )2 ! f0; 1g for S .
such that is Step 3. In this step, we characterize which particles can be added in order to turn into an E L >-uni er of ; satisfying S S . Recall that particles are of the form 9r1: 9rn:A for n 0 role names r1; : : : ; rn and a concept name A. We write such a particle as 9w:A, where w = r1 rn is viewed as a word over the alphabet NR of all role names. If n = 0, then w is the empty word " and 9":A is just A.
Admissible particles are determined by solutions of a system of linear language inclusions. These linear inclusions are of the form
Xi
L0 [ L1X1 [ : : : [ LnXn; (1) where X1; : : : ; Xn are indeterminates, i 2 f1; : : : ; ng, and each Li (i 2 f0; : : : ; ng) is a subset of NR [ f"g. A solution of such an inclusion assigns sets of words (Xi) NR to the indeterminates Xi such that (Xi) L0 [ L1 (X1) [ : : : [ Ln (Xn).
The uni cation problem ; induces a nite system I ; of such inclusions. The indeterminates of I ; are of the form XA, where X 2 Nv and A 2 Nc. For each constant A 2 Nc and each subsumption of the form C1 u : : : u Cn v? X 2 ; , we add the following inclusion to I ; :
XA
fA(C1) [ : : : [ fA(Cn); where fA(C) := >8 frgfA(C0) if C = 9r:C0 >< YA if C = Y is a variable > f"g if C = A >: ; if C 2 Nc n fAg Since ; contains only at atoms, these inclusion are indeed of the form (1).
We call a solution of I ; admissible if, for every variable X 2 Nv, there is a constant A 2 Nc such that (XA) is nonempty. This condition will ensure that we can add enough particles to turn into an E L >-substitution. In order to obtain a substitution at all, only nitely many particles can be added. Thus, we are interested in nite solutions of I ; , i.e., solutions such that all the sets (XA) are nite.
Lemma 4. Let ping for . Then admissible solution.
be a at E L >-uni cation problem and ; has an E L >-uni er with S
a subsumption mapS i I ; has a nite, Proof sketch. Given a ground E L >-uni er of ; with S for each concept variable X and concept constant A occurring in S , we de ne : (XA) := fw 2 NR j 9w:A 2 Part( (X))g: It can then be shown that is a solution of I ; . This solution is nite since any concept term has only nitely many particles, and it is admissible since is an E L >-substitution.
Conversely, let be a nite, admissible solution of I ; . We de ne the substitution by induction on the dependency order > induced by S as follows. Let X be a variable of and assume that (Y ) has already been de ned for all variables Y with X > Y . Then we set
l l (X) :=
(D) u l D2S (X)
A2Nc w2 (XA) 9w:A: Since is nite and admissible, shown that (X) is indeed an E L is a well-de ned E L >-substitution. It can be >-uni er of ; with S S . tu Step 4. In this step we show how to test whether the system I ; of linear language inclusions constructed in the previous step has a nite, admissible solution or not. The main idea is to consider the greatest solution of I ; .
To be more precise, given a system of linear language inclusions I, we can order the solutions of I by de ning 1 2 i 1(X) 2(X) for all indeterminates X of I. Since ;, which assigns the empty set to each indeterminate of I, is a solution of I and solutions are closed under argument-wise union, the following clearly de nes the (unique) greatest solution of I w.r.t. this order: (X) :=
[ solution of I (X): Lemma 5. Let X be an indeterminate in I and If (X) is nonempty, then there is a nite solution nonempty. the maximal solution of I.
of I such that (X) is Proof. Let w 2 (X). We construct the nite solution of I by keeping only the words of length jwj: for all indeterminates Y occurring in I we de ne (Y ) := fu 2 (Y ) j juj jwjg: By de nition, we have w 2 (X). To show that is indeed a solution of I, consider an arbitrary inclusion Y L0 [ L1X1 [ : : : [ LnXn in I, and assume that u 2 (Y ). We must show that u 2 L0 [ L1 (X1) [ : : : [ Ln (Xn). Since u 2 (Y ) and is a solution of I, we have (i) u 2 L0 or (ii) u 2 Li (Xi) for some i; 1 i n. In the rst case, we are done. In the second case, u = u0 for some 2 Li NR [ f"g and u0 2 (Xi). Since ju0j juj jwj, we have u0 2 (Xi), and thus u 2 Li (Xi). tu Lemma 6. There is a nite, admissible solution of I ; i the maximal solution of I ; is admissible.
Proof. If I ; has a nite, admissible solution , then the maximal solution of I ; contains this solution, and is thus also admissible.
Conversely, if is admissible, then (by Lemma 5) for each X 2 Var( ) there
is a constant A(X) and a nite solution X of I ; such that X (XA(X)) 6= ;.
The union of these solutions X for X 2 Var( ) is the desired nite, admissible
solution.
tu
Given this lemma, it remains to show how we can test admissibility of the
maximal solution of I ; . For this purpose, it is obviously su cient to be able
to test, for each indeterminate XA in I ; , whether (XA) is empty or not.
This can be achieved by representing the languages (XA) using alternating
nite automata with "-transitions ("-AFA), which are a special case of two-way
alternating nite automata. In fact, as shown in [
This nishes the description of our E L >-uni cation algorithm. It remains to argue why it is a PSpace decision procedure for E L >-uni ability. Theorem 1. The problem of deciding uni ability in E L > is PSpace-complete.
Proof. Here we only show that the problem is in NPSpace, which is equal to
PSpace by Savitch's theorem [
Let be a at E L >-uni cation problem. By Lemma 3, Lemma 4, and Lemma 6, we know that is E L >-uni able i there is a subsumption mapping for such that the maximal solution of I ; is admissible.
Thus, we rst guess a mapping : At( )2 ! f0; 1g and test whether is a subsumption mapping for . Guessing can clearly be done in NPSpace. For a given mapping , the test whether it is a subsumption mapping for can be done in polynomial time.
From we can rst construct ; and then I ; in polynomial time. Given I ; , we then construct the (polynomially many) "-AFA A(X; A), and test them for emptiness. Since the emptiness problem for "-AFA is in PSpace, this can be achieved within PSpace. Given the results of these emptiness tests, we can then check in polynomial time whether, for each concept variable X of there is a concept constant A of such that (XA) = L(A(X; A)) 6= ;. If this is the case, then is admissible, and thus is E L >-uni able. tu
Uni cation in E L was introduced in [
Surprisingly, it has turned out that the complexity of uni cation in E L >
(PSpace) is considerably higher than of uni cation in E L (NP). From a
theoretical point of view, this result is interesting since it provides us with a natural
example where reducing the expressiveness of a given DL (in a rather minor way)
increases the complexity of the uni ability problem. Regarding the complexity
of uni cation in more expressive DLs, not much is known. If we add negation
to E L, then we obtain the well-known DL ALC, which corresponds to the basic
(multi-)modal logic K [
Apart from its theoretical interest, the result of this paper also has practical
implications. Whereas practically rather e cient uni cation algorithm for E L
can readily be obtained by a translation into SAT [
Another topic for future research is how to actually compute E L >-uni ers
for a uni able E L >-uni cation problem. In principle, our decision procedure
is constructive in the sense that, from appropriate successful runs of the "-AFA
A(X; A), one can construct a nite, admissible solution of I ; , and from this an
E L >-uni er of . However, this needs to be made more explicit, and we need
to investigate what kind of E L >-uni ers can be computed this way.
4 Note that the right-identity rules in SNOMED CT [
Thus, complex role inclusion axioms are not relevant here.