Unification in the Description Logic EL without the Top Concept Franz Baader1? , Nguyen Thanh Binh2 , Stefan Borgwardt1? , and Barbara Morawska1? 1 TU Dresden, Germany, {baader,stefborg,morawska}@tcs.inf.tu-dresden.de 2 ETH Zürich, Switzerland, thannguy@inf.ethz.ch Abstract. Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundan- cies in ontologies. The inexpressive Description Logic EL is of particular interest in this context since, on the one hand, several large biomedical ontologies are defined using EL. On the other hand, unification in EL has recently been shown to be NP-complete, and thus of considerably lower complexity than unification in other DLs of similarly restricted expres- sive 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, remov- ing the top concept from EL makes the unification problem considerably harder. More precisely, we will show that unification in EL without the top concept is PSpace-complete. 1 Introduction Unification in DLs has been proposed in [7] as a novel inference service that can, for example, be used to detect redundancies in ontologies. In this paper, we will look at unification in ontologies expressed in EL. For example, assume that one knowledge engineer defines the concept of female professors as Person u Female u ∃job.Professor, whereas another knowledge engineer represent this notion in a somewhat differ- ent way, e.g., by using the concept term Woman u ∃job.(Teacher u Researcher). These two concept terms are not equivalent, but they are nevertheless meant to represent the same concept. They can obviously be made equivalent by sub- stituting the concept name Professor in the first 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 unifier of the two terms. Such a unifier proposes definitions ? 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 define Woman as Person u Female and Professor as Teacher u Researcher, then the two concept terms from above are equivalent w.r.t. these definitions. In [7] it was shown that, for the DL FL0 , which differs from EL by offering value restrictions (∀r.C) in place of existential restrictions, deciding unifiability is an ExpTime-complete problem. In [4], we were able to show that unification in EL is of considerably lower complexity: the decision problem is “only” NP- complete. The original unification algorithm for EL introduced in [4] was a brutal “guess and then test” NP-algorithm, but we have since then also developed more practical algorithms. On the one hand, in [6] we describe a goal-oriented unification algorithm for EL, in which non-deterministic decisions are only made if they are triggered by “unsolved parts” of the unification problem. On the other hand, in [5], we present an algorithm that is based on a reduction to satisfiability in propositional logic (SAT), and thus allows us to employ highly optimized state-of-the-art SAT solvers for implementing an EL-unification algorithm. However, the large medical ontology SNOMED CT is not formulated in EL, but rather in its sub-logic EL−> , which differs from EL in that the use of the top concept is disallowed. If we employ EL-unification to detect redundancies in (extensions of) SNOMED CT, then a unifier may introduce concept terms that contain the top concept, and thus propose definitions for concept names that are of a form that is not used in SNOMED CT. Apart from this practical motivation for investigating unification in EL−> , we also found it interesting to see how such a small change in the logic influences the unification problem. Surprisingly, it turned out that the complexity of the problem increases considerably (from NP to PSpace). In addition, compared to EL-unification, quite different methods had to be developed to actually solve EL−> -unification problems. In particular, we will show in this paper, that—similar to the case of FL0 -unification—EL−> - unification can be reduced to solving certain language equations. In contrast to the case of FL0 -unification, 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 finite words. Complete proofs of the results presented in this paper can be found in [1]. There we also show PSpace-hardness of EL−> -unification by a reduction of the intersection emptiness problem for finite automata [11, 8]. An extended version of this paper will be published as [2]. 2 The Description Logics EL and EL−> In this paper, we deal with the description logic EL in which concept terms are built from concept names (NC ) and role names (NR ) using the constructors conjunction (u), existential restriction (∃r.C) and the top concept (>). In the restricted description logic EL−> , concept terms may not contain >. As usual, these concepts are interpreted as sets over some domain [3]. An EL-concept term is called an atom iff it is a concept name A ∈ NC or an existential restriction ∃r.D. Concept names and existential restrictions ∃r.D, where D is a concept name or >, are called flat atoms. The set At(C) of atoms of an EL-concept term C consists of all the subterms of C that are atoms. For example, C = A u ∃r.(B u ∃r.>) has the atom set At(C) = {A, ∃r.(B u ∃r.>), B, ∃r.>}. Obviously, any EL-concept term C is a conjunction C = C1 u . . . u Cn of atoms and >. We call the atoms among C1 , . . . , Cn the top-level atoms of C. The EL-concept term C is called flat if all its top-level atoms are flat. Subsumption in EL and EL−> can be characterized as follows [6]: Lemma 1. Let C = A1 u . . . u Ak u ∃r1 .C1 u . . . u ∃rm .Cm and D = B1 u . . . u Bl u∃s1 .D1 u. . .u∃sn .Dn be two EL-concept terms, where A1 , . . . , Ak , B1 , . . . , Bl are concept names. Then C v D iff {B1 , . . . , Bl } ⊆ {A1 , . . . , Ak } and for every j ∈ {1, . . . , n} there exists an i ∈ {1, . . . , m} such that ri = sj and Ci v Dj . In particular, this means that C v D iff for every top-level atom D0 of D there is a top-level atom C 0 of C such that C 0 v D0 . Modulo equivalence, the subsumption relation is a partial order on concept terms. In EL, the top concept > is the greatest element w.r.t. this order. In EL−> , there are many incomparable maximal concept terms. We will see below that these are exactly the EL−> -concept terms of the form ∃r1 . · · · ∃rn .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 EL−> -concept term C is defined as – Part(C) := {C} if C is a concept name, – Part(C) := {∃r.E | E ∈ Part(D)} if C = ∃r.D, – Part(C) := Part(C1 ) ∪ Part(C2 ) if C = C1 u C2 . For example, the particles of C = A u ∃r.(A u ∃r.B) are A, ∃r.A, ∃r.∃r.B. Such particles will play an important role in our EL−> -unification algorithm. The next lemma states that particles are indeed the maximal concept terms w.r.t. to subsumption in EL−> , and that the particles subsuming an EL−> -concept term C are exactly the particles of C. Lemma 2. Let C be an EL−> -concept term and B a particle. 1. If B v C, then B ≡ C. 2. B ∈ Part(C) iff C v B. 3 Unification in EL and EL−> To define unification in EL and EL−> simultaneously, let L ∈ {EL, EL−> }. When defining unification in L, we assume that the set of concepts names is partitioned into a set Nv of concept variables (which may be replaced by sub- stitutions) 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 ∈ Nv . Unification tries to make concept terms equivalent by applying a substitution. Definition 1. An L-unification problem is of the form Γ = {C1 ≡? D1 , . . . , Cn ≡? Dn }, where C1 , D1 , . . . Cn , Dn are L-concept terms. The L-substitution σ is an L-unifier of Γ iff it solves all the equations Ci ≡? Di in Γ , i.e., iff σ(Ci ) ≡ σ(Di ) for i = 1, . . . , n. In this case, Γ is called L-unifiable. 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 iff σ(C) v σ(D). Clearly, every EL−> -unification problem Γ is also an EL-unification problem. Whether Γ is L-unifiable or not may depend, however, on whether L = EL or L = EL−> . As an example, consider the problem Γ := {A v? X, B v? X}, where A, B are distinct concept constants and X is a concept variable. Obviously, the substitution that replaces X by > is an EL-unifier of Γ . However, Γ does not have an EL−> -unifier. In fact, for such a unifier σ, the EL−> -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 = EL and L = EL−> , an L-unification problem Γ has an L-unifier iff it has a ground L-unifier σ 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 flat L-unification problems, i.e., unification problems in which the left- and right-hand sides of equations are flat L-concept terms (see, e.g., [6]). Given a flat L-unification 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(Γ )\Var(Γ ) the set of all non-variable atoms of Γ . EL-unification by guessing acyclic assignments The NP-algorithm for EL-unification introduced in [4] guesses, for every vari- able X occurring in Γ , a set S(X) of non-variable atoms of Γ . Given such an assignment of sets of non-variable atoms to the variables in Γ , we say that the variable X directly depends on the variable Y if Y occurs in an atom of S(X). Let depends on be the transitive closure of directly depends on. If there is no variable that depends on itself, then we call this assignment acyclic. In case the guessed assignment is not acyclic, this run of the NP-algorithm returns “fail.” Otherwise, there exists a strict linear order > on the variables occurring in Γ such that X > Y if X depends on Y . One can then define the substitution γ S induced by the assignment S along this linear order: – If X is the least variable w.r.t. >, then γ S (X) is the conjunction of the elements of S(X), where the empty conjunction is >. 3 Without loss of generality, we assume that Γ contains at least one concept name. – Assume γ S (Y ) is defined for all variables Y < X. If S(X) = {D1 , . . . , Dn }, then γ S (X) := γ S (D1 ) u . . . u γ S (Dn ). The algorithm then tests whether the substitution γ S computed this way is a unifier of Γ . If this is the case, then this run returns γ S ; otherwise, it returns “fail.” In [4] it is shown that Γ is unifiable iff there is a run of this algorithm on input Γ that returns a substitution (which is then an EL-unifier of Γ ). Why this does not work for EL−> The EL-unifiers returned by the EL-unification algorithm sketched above need not be EL−> -unifiers since some of the sets S(X) in the guessed assignment may be empty, in which case γ S (X) = >. This suggests the following simple modification of the above algorithm: require that the guessed assignment is such that all sets S(X) are nonempty. If such an assignment S is acyclic, then the induced substitution γ S is actually an EL−> -substitution, and thus the substi- tutions returned by the modified algorithm are indeed EL−> -unifiers. However, this modified algorithm does not always detect EL−> -unifiability, i.e., it may return no substitution although the input problem is EL−> -unifiable. As an example, consider the EL−> -unification problem Γ := {A u B ≡? Y, B u C ≡? Z, ∃r.Y v? X, ∃r.Z v? X}, 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 ∃r.B, Y to A u B, and Z to B u C is the only EL−> -unifier of Γ . In fact, any EL−> -unifier γ of Γ must map Y to A u B and Z to B u C, and thus satisfy ∃r.(A u B) v γ(X) and ∃r.(B u C) v γ(X). Lemma 1 then yields that the only possible top-level atom of γ(X) is ∃r.B. However, there is no non-variable atom D ∈ NV(Γ ) such that γ(D) is equivalent to ∃r.B. This shows that Γ has an EL−> -unifier, but this unifier cannot be computed by the modified algorithm sketched above. The main idea underlying the EL−> -unification algorithm introduced in the next section is that one starts with an EL-unifier, and then conjoins “appro- priate” particles to the images of the variables that are replaced by > by this unifier. It is, however, not so easy to decide which particles can be added this way without turning the EL-unifier into an EL−> -substitution that no longer solves the unification problem. 4 An EL−> -Unification Algorithm In the following, let Γ be a flat EL−> -unification 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−> -unifiability proceeds in four steps. Step 1. If S is an acyclic assignment guessed by the EL-unification algorithm sketched above, then D ∈ 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 EL−> -unification algorithm starts with guessing subsumptions between arbitrary atoms of Γ . To be more precise, it guesses a mapping τ : At(Γ )2 → {0, 1}, which specifies which subsumptions between atoms of Γ should hold for the EL−> -unifier that it tries to generate: if τ (D1 , D2 ) = 1 for D1 , D2 ∈ At(Γ ), then this means that the search for a unifier 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) := {D ∈ NV(Γ ) | τ (X, D) = 1}, and we require that this assignment is acyclic and induces an EL-unifier of Γ . Definition 2. The mapping τ : At(Γ )2 → {0, 1} is called a subsumption map- ping for Γ if it satisfies the following three conditions: 1. It respects the properties of subsumption in EL: (a) τ (D, D) = 1 for each D ∈ At(Γ ). (b) τ (A1 , A2 ) = 0 for distinct concept constants A1 , A2 ∈ At(Γ ). (c) τ (∃r.C1 , ∃s.C2 ) = 0 for distinct r, s ∈ NR with ∃r.C1 , ∃s.C2 ∈ At(Γ ). (d) τ (A, ∃r.C) = τ (∃r.C, A) = 0 for each constant A ∈ At(Γ ), role name r and variable or constant C with ∃r.C ∈ At(Γ ). (e) If ∃r.C1 , ∃r.C2 ∈ At(Γ ), then τ (∃r.C1 , ∃r.C2 ) = τ (C1 , C2 ). (f ) For all atoms D1 , D2 , D3 ∈ At(Γ ), if τ (D1 , D2 ) = τ (D2 , D3 ) = 1, then τ (D1 , D3 ) = 1. 2. It induces an EL-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 satisfies 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 ∈ 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 EL−> - unification algorithm, it can be shown that the substitution γ τ induced by a subsumption mapping τ for Γ is indeed an EL-unifier of Γ . It should be noted that γ τ need not be an EL−> -unifier of Γ . In addition, γ τ need not agree with τ on every subsumption between atoms of Γ . The reason for this is that τ specifies subsumptions which should hold in the EL−> -unifier of Γ to be constructed. To turn γ τ into such an EL−> -unifier, 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 unification problem that has only variables on the right-hand sides of subsumptions. More precisely, we define ∆Γ,τ := ∆Γ ∪ ∆τ , where ∆Γ := {C1 u . . . u Cn v? X ∈ Γ | X is a variable of Γ }, ∆τ := {C v? X | X is a variable and C an atom of Γ with τ (C, X) = 1}. For an arbitrary EL−> -substitution σ, we define S σ (X) := {D ∈ NV(Γ ) | σ(X) v σ(D)}, and write S τ ≤ S σ if S τ (X) ⊆ S σ (X) for every variable X. The following lemma states the connection between EL−> -unifiability of Γ and of ∆Γ,τ , using the notation that we have just introduced. Lemma 3. Let Γ be a flat EL−> -unification problem. Then the following state- ments are equivalent for any EL−> -substitution σ: 1. σ is an EL−> -unifier of Γ . 2. There is a subsumption mapping τ : At(Γ )2 → {0, 1} for Γ such that σ is an EL−> -unifier of ∆Γ,τ and S τ ≤ S σ . Step 3. In this step, we characterize which particles can be added in order to turn γ τ into an EL−> -unifier σ of ∆Γ,τ satisfying S τ ≤ S σ . Recall that particles are of the form ∃r1 . · · · ∃rn .A for n ≥ 0 role names r1 , . . . , rn and a concept name A. We write such a particle as ∃w.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 ∃ε.A is just A. Admissible particles are determined by solutions of a system of linear lan- guage inclusions. These linear inclusions are of the form Xi ⊆ L0 ∪ L1 X1 ∪ . . . ∪ Ln Xn , (1) where X1 , . . . , Xn are indeterminates, i ∈ {1, . . . , n}, and each Li (i ∈ {0, . . . , n}) is a subset of NR ∪ {ε}. 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 unification problem ∆Γ,τ induces a finite system IΓ,τ of such inclusions. The indeterminates of IΓ,τ are of the form XA , where X ∈ Nv and A ∈ Nc . For each constant A ∈ Nc and each subsumption of the form C1 u . . . u Cn v? X ∈ ∆Γ,τ , we add the following inclusion to IΓ,τ : XA ⊆ fA (C1 ) ∪ . . . ∪ fA (Cn ), where {r}fA (C 0 ) if C = ∃r.C 0    YA if C = Y is a variable  fA (C) :=   {ε} if C = A ∅ if C ∈ Nc \ {A}  Since ∆Γ,τ contains only flat atoms, these inclusion are indeed of the form (1). We call a solution θ of IΓ,τ admissible if, for every variable X ∈ Nv , there is a constant A ∈ Nc such that θ(XA ) is nonempty. This condition will ensure that we can add enough particles to turn γ τ into an EL−> -substitution. In order to obtain a substitution at all, only finitely many particles can be added. Thus, we are interested in finite solutions of IΓ,τ , i.e., solutions θ such that all the sets θ(XA ) are finite. Lemma 4. Let Γ be a flat EL−> -unification problem and τ a subsumption map- ping for Γ . Then ∆Γ,τ has an EL−> -unifier σ with S τ ≤ S σ iff IΓ,τ has a finite, admissible solution. Proof sketch. Given a ground EL−> -unifier σ of ∆Γ,τ with S τ ≤ S σ , we define for each concept variable X and concept constant A occurring in Γ : θ(XA ) := {w ∈ NR∗ | ∃w.A ∈ Part(σ(X))}. It can then be shown that θ is a solution of IΓ,τ . This solution is finite since any concept term has only finitely many particles, and it is admissible since σ is an EL−> -substitution. Conversely, let θ be a finite, admissible solution of IΓ,τ . We define the sub- stitution σ by induction on the dependency order > induced by S τ as follows. Let X be a variable of Γ and assume that σ(Y ) has already been defined for all variables Y with X > Y . Then we set l l l σ(X) := σ(D) u ∃w.A. D∈S τ (X) A∈Nc w∈θ(XA ) Since θ is finite and admissible, σ is a well-defined EL−> -substitution. It can be shown that σ(X) is indeed an EL−> -unifier of ∆Γ,τ with S τ ≤ S σ . t u 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 finite, 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 defining θ1 ⊆ θ2 iff θ1 (X) ⊆ θ2 (X) for all indeter- minates 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 defines the (unique) greatest solution θ∗ of I w.r.t. this order: [ θ∗ (X) := θ(X). θ solution of I Lemma 5. Let X be an indeterminate in I and θ∗ the maximal solution of I. If θ∗ (X) is nonempty, then there is a finite solution θ of I such that θ(X) is nonempty. Proof. Let w ∈ θ∗ (X). We construct the finite solution θ of I by keeping only the words of length |w|: for all indeterminates Y occurring in I we define θ(Y ) := {u ∈ θ∗ (Y ) | |u| ≤ |w|}. By definition, we have w ∈ θ(X). To show that θ is indeed a solution of I, consider an arbitrary inclusion Y ⊆ L0 ∪ L1 X1 ∪ . . . ∪ Ln Xn in I, and assume that u ∈ θ(Y ). We must show that u ∈ L0 ∪ L1 θ(X1 ) ∪ . . . ∪ Ln θ(Xn ). Since u ∈ θ∗ (Y ) and θ∗ is a solution of I, we have (i) u ∈ L0 or (ii) u ∈ Li θ∗ (Xi ) for some i, 1 ≤ i ≤ n. In the first case, we are done. In the second case, u = αu0 for some α ∈ Li ⊆ NR ∪ {ε} and u0 ∈ θ∗ (Xi ). Since |u0 | ≤ |u| ≤ |w|, we have u0 ∈ θ(Xi ), and thus u ∈ Li θ(Xi ). t u Lemma 6. There is a finite, admissible solution of IΓ,τ iff the maximal solution θ∗ of IΓ,τ is admissible. Proof. If IΓ,τ has a finite, 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 ∈ Var(Γ ) there is a constant A(X) and a finite solution θX of IΓ,τ such that θX (XA(X) ) 6= ∅. The union of these solutions θX for X ∈ Var(Γ ) is the desired finite, admissible solution. t u Given this lemma, it remains to show how we can test admissibility of the max- imal solution θ∗ of IΓ,τ . For this purpose, it is obviously sufficient 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 finite automata with ε-transitions (ε-AFA), which are a special case of two-way alternating finite automata. In fact, as shown in [10], the emptiness problem for two-way alternating finite automata (and thus also for ε-AFA) is in PSpace. Lemma 7. For each indeterminate XA in IΓ,τ , we can construct in polynomial time in the size of IΓ,τ an ε-AFA A(X, A) such that the language L(A(X, A)) accepted by A(X, A) is equal to θ∗ (XA ), where θ∗ denotes the maximal solution of IΓ,τ . This finishes the description of our EL−> -unification algorithm. It remains to argue why it is a PSpace decision procedure for EL−> -unifiability. Theorem 1. The problem of deciding unifiability in EL−> is PSpace-complete. Proof. Here we only show that the problem is in NPSpace, which is equal to PSpace by Savitch’s theorem [13]. PSpace-hardness is shown in [1, 2]. Let Γ be a flat EL−> -unification problem. By Lemma 3, Lemma 4, and Lemma 6, we know that Γ is EL−> -unifiable iff there is a subsumption mapping τ for Γ such that the maximal solution θ∗ of IΓ,τ is admissible. Thus, we first guess a mapping τ : At(Γ )2 → {0, 1} 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 first 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 EL−> -unifiable. t u 5 Conclusion Unification in EL was introduced in [4] as an inference service that can sup- port the detection of redundancies in large biomedical ontologies, which are frequently written in this DL. Motivated by the fact that the large medical ontology SNOMED CT actually does not use the top concept available in EL, we have in this paper investigated unification in EL−> , which is obtained from EL by removing the top concept. More precisely, SNOMED CT is a so-called acyclic EL−> -TBox,4 rather than a collection of EL−> -concept terms. However, as shown in [6], acyclic TBoxes can be easily handled by a unification algorithm for concept terms. Surprisingly, it has turned out that the complexity of unification in EL−> (PSpace) is considerably higher than of unification in EL (NP). From a theo- retical 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 unifiability problem. Regarding the complexity of unification in more expressive DLs, not much is known. If we add negation to EL, then we obtain the well-known DL ALC, which corresponds to the basic (multi-)modal logic K [14]. 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 [17]. These undecidabil- ity results also imply undecidability of unification in some expressive DLs (e.g., in SHIQ [9]). Apart from its theoretical interest, the result of this paper also has practical implications. Whereas practically rather efficient unification algorithm for EL can readily be obtained by a translation into SAT [5], it is not so clear how to turn the PSpace algorithm for EL−> -unification introduced in this paper into a practically useful algorithm. One possibility could be to use a SAT modulo theories (SMT) approach [12]. The idea is that the SAT solver is used to generate all possible subsumption mappings for Γ , and that the theory solver tests the system IΓ,τ induced by τ for the existence of a finite, admissible solution. How well this works will mainly depend on whether we can develop such a theory solver that satisfies well all the requirements imposed by the SMT approach. Another topic for future research is how to actually compute EL−> -unifiers for a unifiable EL−> -unification 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 finite, admissible solution of IΓ,τ , and from this an EL−> -unifier of Γ . However, this needs to be made more explicit, and we need to investigate what kind of EL−> -unifiers can be computed this way. 4 Note that the right-identity rules in SNOMED CT [15] are actually not expressed using complex role inclusion axioms, but through the SEP-triplet encoding [16]. Thus, complex role inclusion axioms are not relevant here. References 1. Franz Baader, Nguyen Thanh Binh, Stefan Borgwardt, and Barbara Morawska. Unification in the description logic EL without the top concept. LTCS-Report 11-01, TU Dresden, Dresden, Germany, 2011. See http://lat.inf.tu-dresden.de/research/reports.html. 2. Franz Baader, Nguyen Thanh Binh, Stefan Borgwardt, and Barbara Morawska. Unification in the description logic EL without the top concept. In Proc. of the 23rd Int. Conf. on Automated Deduction (CADE 23), Springer LNCS, 2011. To appear. 3. Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementa- tion, and Applications. Cambridge University Press, 2003. 4. Franz Baader and Barbara Morawska. Unification in the description logic EL. In Proc. of the 20th Int. Conf. on Rewriting Techniques and Applications (RTA 2009), Springer LNCS 5595, pages 350–364, 2009. 5. Franz Baader and Barbara Morawska. SAT encoding of unification in EL. In Proc. of the 17th Int. Conf. on Logic for Programming, Artifical Intelligence, and Reasoning (LPAR-17), Springer LNCS 6397, pages 97–111, 2010. 6. Franz Baader and Barbara Morawska. Unification in the description logic EL. Logical Methods in Computer Science, 6(3), 2010. 7. Franz Baader and Paliath Narendran. Unification of concept terms in description logics. Journal of Symbolic Computation, 31(3):277–305, 2001. 8. Michael R. Garey and David S. Johnson. Computers and Intractability — A guide to NP-completeness. W. H. Freeman and Company, San Francisco (USA), 1979. 9. Ian Horrocks, Ulrike Sattler, and Stefan Tobies. Practical reasoning for very ex- pressive description logics. Logic Journal of the IGPL, 8(3):239–264, 2000. 10. Tao Jiang and B. Ravikumar. A note on the space complexity of some decision problems for finite automata. Information Processing Letters, 40:25–31, 1991. 11. Dexter Kozen. Lower bounds for natural proof systems. Annual IEEE Symposium on Foundations of Computer Science, pages 254–266, 1977. 12. Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T ). J. ACM, 53(6):937–977, 2006. 13. Walter J. Savitch. Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 4(2):177–192, 1970. 14. Klaus Schild. A correspondence theory for terminological logics: Preliminary re- port. In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI’91), pages 466–471, 1991. 15. Kent A. Spackman. Managing clinical terminology hierarchies using algorithmic calculation of subsumption: Experience with SNOMED-RT. Journal of the Amer- ican Medical Informatics Association, 2000. Fall Symposium Special Issue. 16. Boontawee Suntisrivaraporn, Franz Baader, Stefan Schulz, and Kent Spackman. Replacing SEP-triplets in SNOMED CT using tractable description logic opera- tors. In Proc. of the 11th Conf. on Artificial Intelligence in Medicine (AIME’07), Springer LNCS 4594, pages 287–291, 2007. 17. Frank Wolter and Michael Zakharyaschev. Undecidability of the unification and admissibility problems for modal and description logics. ACM Transactions on Computational Logic, 9(4), 2008.