=Paper=
{{Paper
|id=None
|storemode=property
|title=Unification in the Description Logic EL without the Top Concept
|pdfUrl=https://ceur-ws.org/Vol-745/paper_5.pdf
|volume=Vol-745
|dblpUrl=https://dblp.org/rec/conf/dlog/BaaderBBM11
}}
==Unification in the Description Logic EL without the Top Concept==
https://ceur-ws.org/Vol-745/paper_5.pdf
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.