=Paper=
{{Paper
|id=Vol-2954/paper-4
|storemode=property
|title=Restricted Unification in the DL EL
|pdfUrl=https://ceur-ws.org/Vol-2954/paper-4.pdf
|volume=Vol-2954
|authors=Franz Baader,Maryam Rostamigiv
|dblpUrl=https://dblp.org/rec/conf/dlog/BaaderR21
}}
==Restricted Unification in the DL EL==
https://ceur-ws.org/Vol-2954/paper-4.pdf
Restricted Unification in the DL EL
Franz Baader1 and Maryam Rostamigiv2
1
Theoretical Computer Science, TU Dresden, Dresden, Germany
franz.baader@tu-dresden.de
2
Département d’Informatique, Paul Sabatier University, Toulouse, France
Maryam.Rostamigiv@irit.fr
Abstract. Research on unification in Description Logic (DL) has con-
centrated on the lightweight DLs FL0 and EL. For both DLs, the unifi-
cation type is zero, which is the worst possible type. The complexity of
deciding unifiability is ExpTime-complete for FL0 and NP-complete for
EL. In a recent paper, we have shown that, for FL0 , both the unifica-
tion type and the complexity of the decision problem can be improved
by considering restricted versions of the unification problem where ei-
ther the role depth of concepts is restricted syntactically or the length
of role paths in interpretations is restricted semantically. In the present
paper, we show that no such improvements can be obtained for EL: both
in the syntactically and in the semantically restricted case, the unifica-
tion type stays zero, and the complexity of the decision problem stays
NP-complete.
1 Introduction
Unification theory [13] investigates the unification properties of equational theo-
ries (such as associativity and commutativity of a binary function symbol). Given
an equational theory E and terms s, t, the decision problem asks whether s and t
can be made equal modulo E by replacing variables by terms, i.e., whether there
is a substitution σ such that σ(s) =E σ(t). In addition to testing unifiability,
one is also interested in computing a small representation of all unifiers, i.e., a
set of unifiers from which all unifiers can be obtained by instantiation. Such a
set is called a complete set of unifiers. From a practical point of view, it is useful
to have finite complete sets of unifiers. If the theory has unification type zero,
then there is a unification problem w.r.t. this theory such that every complete
set of unifiers is redundant in the sense that it contains unifiers that are in an
instance relationship, which implies that the unification problem cannot have a
finite complete set of unifiers. Unification in modal and description logics [5] can
be seen as a special case of unification w.r.t. an equational theory, where the
theory axiomatizes equivalence of formulae/concepts (viewed as terms) in the
respective logic.
Copyright c 2021 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0).
2 F. Baader and M. Rostamigiv
Unification of concept patterns has been proposed as a nonstandard infer-
ence service in DL that can, for instance, be used to detect redundancies in
ontologies. For example, assume that one ontologist describes the medical con-
cept of myocarditis by the EL concept HeartDisease u ∃cause.Virus whereas
another one describes it by ViralInfection u ∃location.Heart. These two con-
cepts are not equivalent, but they can be unified (i.e., made equivalent) if we
view HeartDisease and ViralInfection as variables that can be replaced by com-
plex concepts. In fact, replacing HeartDisease with Disease u ∃location.Heart
in the first concept yields Disease u ∃location.Heart u ∃cause.Virus, and re-
placing ViralInfection with Disease u ∃cause.Virus in the second concept yields
Disease u ∃cause.Virus u ∃location.Heart. These two concepts are clearly equiv-
alent, and they actually yield an appropriate description of myocarditis.
For the DL FL0 , which has the concept constructors conjunction (u), value
restriction (∀r.C), and top concept (>), unification was investigated in detail
in [12]. It was shown there that unification in FL0 is ExpTime-complete and of
unification type zero. The DL EL, which has the concept constructors conjunc-
tion (u), existential restriction (∃r.C), and top concept (>), also has unification
type zero, but the complexity of the decision problem is lower than for FL0 : it
is “only” NP-complete for EL [11].
In [3], we investigate two kinds of restrictions on unification in FL0 . On the
one hand, we syntactically restrict the role depth (i.e., the maximal nesting of
value restrictions) in the concepts obtained by applying a unifier to be bounded
by a natural number k ≥ 1. This restriction was motivated by a similar restriction
used in research on least common subsumers (lcs) [19], where imposing a bound
on the role depth guarantees the existence of the lcs also in the presence of a
(possibly cyclic) terminology. Also note that such a restriction was used in [16] for
the equational theory ACh, for which unification is known to be undecidable [18].
It is shown in [16] that the problem becomes decidable if a bound on the maximal
nesting of applications of homomorphisms is imposed. On the other hand, we
consider in [3] a semantic restriction where, when defining the semantics of
concepts, only interpretations for which the length of role paths is bounded by
a given number k are considered. A similar restriction (for k = 1) was employed
in [14] to improve the unification type from type zero for the modal logic K [15]
to finitary for K + ⊥, which means that unification problems always have a
finite complete set of unifiers in this extension of K. We show in [3] that both the
syntactic and the semantic restriction ensures that the unification type of FL0
improves from type zero to finitary. Regarding the decision problem, we show
that the complexity depends on whether the bound k is assumed to be encoded
in unary or binary. For binary encoding of k, the complexity stays ExpTime,
whereas for unary coding it drops from ExpTime to PSpace. This is again the
case both for the syntactic and the semantic restriction.
In the present paper, we investigate whether similar improvements of the
unification type and the complexity of the decision problem can be obtained
for the DL EL. Surprisingly, the answer to this question is “no.” Both in the
syntactically and in the semantically restricted case, the unification type stays
Restricted Unification in the DL EL 3
zero, and the complexity of the decision problem stays NP-complete for EL. This
demonstrates that the reason for type zero and the complexity lower bound
to hold are different for FL0 and EL. Whereas in FL0 they depend on the
possibility of arbitrarily deep nesting of role restrictions, this is not the case for
EL. In fact, we will see that for EL already a nesting depth of k = 1 suffices to
obtain type zero and NP-hardness.
2 The DL EL and Restrictions
Starting with mutually disjoint countably infinite sets NC and NR of concept
and role names, the set of EL concepts is inductively defined as follows:
– > (top concept) and every concept name A ∈ NC is an EL concept,
– if C, D are EL concepts and r ∈ NR is a role name, then C uD (conjunction)
and ∃r.C (existential restriction) are EL concepts.
The semantics of EL concepts is defined using interpretations I = (∆I , ·I )
consisting of a non-empty domain ∆I and an interpretation function ·I that
assigns a set AI ⊆ ∆I to each concept name A, and a binary relation rI ⊆
∆I × ∆I to each role name r. This function is extended to EL concepts as
follows:
>I = ∆I and (C u D)I = C I ∩ DI ,
(∃r.C)I = {x ∈ ∆I | ∃y ∈ ∆I : (x, y) ∈ rI ∧ y ∈ C I }.
Given two EL concepts C and D, we say that C is subsumed by D (written
C v D) if C I ⊆ DI holds for all interpretations I, and that C is equivalent to
D (written C ≡ D) if C v D and D v C.
It is well known that subsumption (and thus also equivalence) of EL concepts
can be decided in polynomial time. This was first shown in [7] based on the notion
of a homomorphism between trees representing concepts, but it is also an easy
consequence of the following recursive characterization of subsumption.
Lemma 1 ([11]). Let C = A1 u . . . u Ak u ∃r1 .C1 u . . . u ∃rm .Cm and D =
B1 u . . . u B` u ∃s1 .D1 u . . . u ∃sn .Dn , where A1 , . . . , Ak , B1 , . . . , B` are concept
names. Then C v D iff {B1 , . . . , B` } ⊆ {A1 , . . . , Ak } and for every j, 1 ≤ j ≤ n,
there exists an i, 1 ≤ i ≤ m, such that ri = sj and Ci v Dj .
2.1 Syntactically Restricting the Role Depth
The role depth of an EL concept is the maximal nesting of existential restrictions
in this concept. To be more precise, the role depth rd (C) of the EL concept C
is defined by induction:
– rd (>) = rd (A) = 0 for all A ∈ NC ,
– rd (C u D) = max(rd (C), rd (D)) and rd (∃r.C) = 1 + rd (C).
4 F. Baader and M. Rostamigiv
Using Lemma 1, it is easy to see that C v D implies rd (C) ≥ rd (D). Thus, the
role depth of EL concepts is preserved under equivalence.
We are now ready to define our first restricted version of subsumption and
equivalence in EL. For an integer k ≥ 1 and EL concepts C and D, we define
subsumption and equivalence restricted to concepts of role depth ≤ k as follows:
– C vksyn D if C v D and rd (C) ≤ k,
– C ≡ksyn D if C vksyn D and D vksyn C.
The effect of this definition is that subsumption and equivalence can only hold
for concepts that satisfy the restriction of the role depth by k. For concepts
satisfying this syntactic restriction, the relations vksyn and ≡ksyn coincide with
the classical subsumption and equivalence relations on EL concepts.
2.2 Semantically Restricting the Length of Role Paths
For an integer n ≥ 1 and a given interpretation I = (∆I , ·I ), a role path of
length n is a sequence d0 , r1 , d1 , . . . , dn−1 , rn , dn , where d0 , . . . , dn are elements
of ∆I , r1 , . . . , rn are role names, and (di−1 , di ) ∈ riI holds for all i = 1, . . . , n.
The interpretation I is called k-restricted if it does not admit any role paths of
length > k.
For an integer k ≥ 1 and EL concepts C and D, we define subsumption and
equivalence restricted to interpretations with role paths of length ≤ k as follows:
– C vksem D if C I ⊆ DI holds for all k-restricted interpretations I,
– C ≡ksem D if C vksem D and D vksem C.
The effect of this semantic restriction is that concepts of role depth > k are
always interpreted as empty sets, i.e., if I is a k-restricted interpretation and
C an EL concept such that rd (C) > k, then C I = ∅. The following lemma is
an easy consequence of this fact, where ⊥ denotes the bottom concept, which is
interpreted as ⊥I = ∅ in every interpretation I.
Lemma 2. Let k ≥ 1 and C, D be EL concepts. Then C ≡ksem ⊥ iff rd (C) > k,
and C ≡ksem D iff
– rd (C) > k and rd (D) > k, or
– rd (C) ≤ k, rd (D) ≤ k, and C ≡ D.
3 Unification in EL
In unification, we consider concepts that may contain variables, which can be
replaced by concepts. More formally, we introduce a countably infinite set NV
of concept variables, which is disjoint with NC and NR . An EL concept pattern
is an EL concept that is constructed using NC ∪ NV as concept names. The
semantics of concept patterns is defined as for concepts, i.e., concept variables
are treated like concept names when defining the semantics. This way, the notions
Restricted Unification in the DL EL 5
of subsumption and equivalence (both in the restricted and in the unrestricted
setting) transfer from concepts to concept patterns in the obvious way.
A substitution σ is a mapping from NV into the set of all EL concept patterns
such that dom(σ) := {X ∈ NV | σ(X) 6= X} is finite. This mapping is extended
to concept patterns in the obvious way:
– σ(A) := A for all A ∈ NC ∪ {>},
– σ(C u D) := σ(C) u σ(D) and σ(∃r.C) := ∃r.σ(C).
An EL unification problem is an equation of the form C ?≡ D where C, D are
EL concept patterns. A unifier (or solution) of this equation is a substitution σ
such that σ(C) ≡ σ(D).
Example 3. Consider the EL unification problem
∃r.X u ∃s.∃r.A ?≡ ∃r.∃s.Y u ∃s.Y.
It is easy to see that (up to equivalence and restricted to the variables X, Y )
the substitution σex with dom(σex ) = {X, Y }, σex (X) = ∃s.∃r.A, and σex (Y ) =
∃r.A is the only unifier of this problem.
3.1 The Unification Type
When considering the unification type of an equational theory or logic, one is
interested in the question of whether all unifiers of a given unification problem
can be represented as instances of a finite set of unifiers, where the instance
relation between unifiers is defined as follows: given unifiers σ, θ of C ?≡D, we say
that θ is an instance of σ if there is a substitution λ such that θ(X) ≡ λ(σ(X))
for all variables X occurring in C or D.
A set of unifiers M of an EL unification problem C ?≡ D is complete if any
unifier of C ?≡ D is an instance of an element of M . This set is minimal if
no two distinct elements of M are comparable w.r.t. the instance relation. The
unification problem C ?≡ D has type zero if it does not have a minimal complete
set of unifiers. Note that this implies that C ?≡ D does not have a finite complete
set of unifiers since such a set could be made minimal by removing unifiers that
are instances of others [13]. Saying that EL has unification type zero means
that there is an EL unification problem that has type zero. Thus, the following
proposition implies that EL indeed has unification type zero.
Proposition 4 ([11]). Let X, Y be concept variables. The EL unification prob-
lem X u ∃r.Y ?≡ ∃r.Y has unification type zero.
The proof of this proposition given in [11], which shows that any complete
set of unifiers M of X u ∃r.Y ?≡ ∃r.Y is non-minimal, proceeds as follows:
1. It observes that the substitution τ with τ (X) = ∃r.A and τ (Y ) = A is a
unifier, and thus there must be an element σ of M such that τ is an instance
of σ. It shows that this unifier σ satisfies σ(X) 6≡ > and σ(X) 6≡ ∃r.>.
6 F. Baader and M. Rostamigiv
2. It then proves that the substitution σ
b defined as
b(X) := σ(X) u ∃r.Z,
σ
where Z is a new variable,
b(Y ) := σ(Y ) u Z,
σ
is a unifier of X u ∃r.Y ?≡ ∃r.Y that has σ as an instance.
3. Since M is complete, it concludes that there is a unifier θ in M such that σ b
is an instance of θ. Since the instance relation is transitive, this implies that
σ is an instance of θ.
4. Using the fact that σ(X) 6≡ > and σ(X) 6≡ ∃r.>, it proves that θ cannot be
equal to σ, and concludes non-minimality of M .
We will show later that this proof also works in the restricted case.
3.2 The Decision Problem
NP-hardness already holds for the case of matching, where we call an EL uni-
fication problem of the form C ?≡ D a matching problem if D does not contain
concept variables. A unifier of a matching problem is also called matcher. NP-
hardness of matching can be shown by a reduction from SAT, i.e., satisfiability
of propositional formulae. In the literature, one can actually find two such re-
ductions with different characteristics:
(R1) In [6], a given propositional formula φ is translated into an EL matching
problem C ?≡ D such that the role depth of both C and D is 1, and the
number of different role names occurring in C and D is linear in the size
of φ.
(R2) In [17] (proof of Corollary 6.3.4, pages 185 and 186), a given propositional
formula φ is translated into an EL matching problem C ?≡ D such that the
role depth of both C and D is linear in the size of φ, and C, D contain only
4 different role names.
For the case of matching, an NP-upper bound was also shown in [6,17]. It
took almost ten years before an NP-upper bound for unification in EL could be
proved in [9,11].
Theorem 5 ([9,11]). Unification in EL is NP-complete.
Showing the NP-upper bound for unification in EL is more involved than
proving the lower bound, though the original proof given in [9,11] was simplified
in later work [10,1]. The basic idea underlying the proof is to show the following:
1. Every solvable EL unification problem C ?≡ D has a local unifier, i.e., a
unifier that is a local substitution. Intuitively, local substitutions are built
from subconcepts of the concepts C, D (see below for more details).
2. Polynomially large representations of local substitutions can be guessed by
a non-deterministic procedure in polynomial time.
3. Given such a representation of a local substitution σ, it can be checked in
polynomial time whether σ is a unifier of C ?≡ D.
Restricted Unification in the DL EL 7
To be more precise, it is shown in [9,11,1] that a given EL unification problem
C ?≡ D determines a set of flat atoms At(C, D), whose cardinality is linear in
the size of the problem. A flat atom is a concept name, a concept variable, or
an existential restriction of the form ∃r.E, where E is either a concept name
or a concept variable. Such an atom is called non-variable if it is not a concept
variable. The subset of non-variable atoms in At(C, D) is denoted as At nv (C, D).
Local substitutions are induced by assignments S, which assign subsets SX
of At nv (C, D) to the concept variables occurring on C, D. To induce a local
substitution, such an assignment needs to be acyclic, which means that the
transitive closure >S of
OS := {(X, Y ) | X, Y are variables in C or D and Y occurs in SX }
is irreflexive (and thus a partial order). Any acyclic assignment S induces a
unique substitution σS , which can be defined by induction along >S :
d
– If X is a minimal variable w.r.t. >S , then σS (X) := E∈SX E.
– Assume that d σS (Y ) is already defined for all Y such that X >S Y . Then
σS (X) := E∈SX σS (E).
A substitution σ is called local if it is of this form, i.e., if there is an acyclic
assignment S such that σ = σS . If the unifier σ of C ?≡ D is a local substitution,
then it is called a local unifier.
Whereas assignments are of size polynomial in the size of the input unifi-
cation problem C ?≡ D (and thus can be guessed by an NP procedure), local
substitutions may assign exponentially large concepts to a variable. Neverthe-
less, given an acyclic assignment S, one can check in polynomial time whether
σS is a unifier, basically by viewing the assignment as an acyclic TBox (see [11]
for details).
The proof that every solvable EL unification problem C ?≡D has a local unifier
given in [11] proceeds in two steps. First, it uses component-wise subsumption
to define an order on substitutions:
σ θ iff σ(X) v θ(X) holds for all variables X occurring in C, D,
σ θ iff σ θ and θ 6 σ.
The unifier σ of C ?≡ D is called minimal if there is no unifier θ of C ?≡ D
such that σ θ. It is then shown in [11] that the pre-order is well-founded,
which immediately implies that very solvable EL unification problem C ?≡ D
has a minimal unifier. The second step, which is considerably more involved, is
then to prove that every minimal unifier is local (see Proposition 5.11 in [11]). A
direct proof that every solvable EL unification problem has a local unifier that
does not use minimal unifiers can be found in [1].
4 Syntactically Restricted Unification in EL
For an integer k ≥ 1, a syntactically k-restricted unification problem is an equa-
k
tion of the form C ?≡syn D, where C, D are EL concept patterns. A unifier of
8 F. Baader and M. Rostamigiv
this equation (also called syntactically k-restricted unifier ) is a substitution σ
such that σ(C) ≡ksyn σ(D).
If we view the unification problem in Example 3 as a syntactically k-restricted
unification problem, then it does not have a solution for k ≤ 2, but the substi-
tution σex is a syntactically k-restricted unifier of this problem for all k ≥ 3.
The following lemma is an immediate consequence of the definition of ≡ksyn
and the fact that rd (σ(X)) ≤ rd (σ(D)) for every substitution σ and every con-
cept variable X occurring in the EL concept D.
k
Lemma 6. If σ is a syntactically k-restricted unifier of C ?≡syn D, then σ is a
unifier of C ?≡ D and rd (σ(X)) ≤ k for every concept variable X occurring in
C or D.
Consequently, the instance relation on syntactically k-restricted unifiers (which
is defined using ≡ksyn ) coincides with the instance relation on unifiers (which is
defined using ≡). However, the set of syntactically k-restricted unifiers may of
course be a strict subset of the set of unrestricted unifiers. For this reason, it is
not immediately clear that type zero transfers from unification to syntactically
k-restricted unification. To see that this is nevertheless the case, one needs to
look more closely at the proof of Proposition 4 sketched in the previous section.
Proposition 7. Let X, Y be concept variables. The syntactically k-restricted EL
k
unification problem X u∃r.Y ?≡syn ∃r.Y has unification type zero for every k ≥ 1.
Proof. Similarly to the proof of Proposition 4, we consider an arbitrary complete
k
set M of syntactically k-restricted unifiers of X u ∃r.Y ?≡syn ∃r.Y . We show that
all the steps made in this proof also work in the syntactically k-restricted case.
1. The unifier τ with τ (X) = ∃r.A and τ (Y ) = A considered in the first step of
that proof is clearly also a syntactically k-restricted unifier for every k ≥ 1.
Since M is complete for such unifiers, τ is an instance1 of an element σ ∈ M .
As before, we conclude that σ satisfies σ(X) 6≡ > and σ(X) 6≡ ∃r.>.
2. Since σ is a syntactically k-restricted unifier, the same is true for the substi-
tution σb constructed in the second step. In fact, we already know that σ b is
a unifier, and the concepts
b(X u ∃r.Y ) = σ(X) u ∃r.Z u ∃r.(σ(Y ) u Z) and σ
σ b(∃r.Y ) = ∃r.(σ(Y ) u Z)
k
have role depth 1 since σ is a syntactically k-restricted unifier of Xu∃r.Y ?≡syn
∃r.Y , which implies rd (σ(X)) ≤ 1 and rd (σ(Y )) = 0.
3. The third step works as above, but we now also know that the unifier θ ∈ M
that has σ as an instance is syntactically k-restricted.
4. The proof that σ and θ cannot be equal again works as for the unrestricted
case since the same notion of instance is employed, due to Lemma 6.
1
Recall that, by Lemma 6, we can assume that this is the classical instance relation.
Restricted Unification in the DL EL 9
This finishes the proof that M cannot be minimal. Since M was chosen as an
k
arbitrary complete set of syntactically k-restricted unifiers of X u∃r.Y ?≡syn ∃r.Y ,
this shows that this unification problem has unification type zero. t
u
Theorem 8. Syntactically k-restricted EL unification has unification type zero
for any k ≥ 1.
Let us now turn to the complexity of the decision problem. In this context, one
can either assume that the bound k is fixed, or that it is part of the input. In the
latter case, one can distinguish between unary and binary coding of the number
k. We want to show that the same reductions from SAT as in the unrestricted
setting can be used to show NP-hardness of the matching problem. For this, the
observations made in the next lemma are useful.
k
Lemma 9. Let C ?≡syn D be a syntactically k-restricted EL matching problem.
k
1. If rd (D) > k, then C ?≡syn D does not have a solution.
k
2. Otherwise, a substitution σ is a syntactically k-restricted matcher of C ?≡syn
D iff it is a matcher of C ?≡ D.
Consequently, the reduction (R1) works for any fixed k ≥ 1 since the concept
D used in that reduction has role depth 1. However, this reduction requires an
unbounded supply of role names.
Proposition 10. For every fixed k ≥ 1, syntactically k-restricted matching is
NP-hard if the number of available role names is not bounded by a finite number.
The reduction (R2) requires only four role names, but the role depth of D is
linear in the size of the propositional formula. Thus, this reduction only works if
we assume the bound k to be part of the input, but the reduction is polynomial
even if unary representation of k is assumed.
Proposition 11. Syntactically k-restricted matching is NP-hard even if only
four role names are available and k is encoded in unary.
We show the NP-upper bound for the most complex case of unification where
k is part of the input and assumed to be encoded in binary. The idea is to employ
basically the same NP procedure as in the unrestricted case, but additionally
check whether the restriction of the role depth is satisfied. Given a syntactically
k
k-restricted unification problem C ?≡syn D, we
1. guess a local substitution σ in non-deterministic polynomial time;
2. check whether σ(C) ≡ σ(D) and rd (σ(C)) ≤ k.
To see that the second test checking the bound on the role depth can also be
realized in polynomial time, it is sufficient to prove the following lemma.
Lemma 12. Let S be an acyclic assignment for the unification problem C ?≡ D.
Then we can compute rd (σS (X)) for every concept variable X occurring in C, D
in time polynomial in the size of C ?≡ D.
10 F. Baader and M. Rostamigiv
Proof. This can easily be shown by induction along >S , following the inductive
definition of the substitution σS . t
u
It remains to show that this NP procedure is complete, i.e., that it is really the
k
case that any solvable syntactically k-restricted unification problem C ?≡syn D
has a local substitution as a solution. We already know (see Section 3) that, for
any unifier σ of C ?≡ D, there is a minimal unifier θ of C ?≡ D such that σ θ.
In addition, θ is local. Using the fact that E v F implies rd (E) ≥ rd (F ), we
can conclude that, if σ is a syntactically k-restricted unifier, then so is θ. This
completes the proof of completeness.
Theorem 13. Syntactically k-restricted unification in EL is NP-complete.
5 Semantically Restricted Unification in EL
For an integer k ≥ 1, a semantically k-restricted unification problem is an equa-
k
tion of the form C ?≡sem D, where C, D are EL concept patterns. A unifier of
this equation (also called semantically k-restricted unifier ) is a substitution σ
such that σ(C) ≡ksem σ(D).
In contrast to the syntactic case, solvability in the semantically k-restricted
setting does not imply solvability in the unrestricted setting. For example, ∃r.X ?≡
∃s.X for distinct role names r, s clearly does not have a solution, but the substitu-
tion σ with σ(X) := ∃r.A is a solution if we view this equation as a semantically
1-restricted unification problem. More generally, the following holds.
k
Lemma 14. If C, D both contain concept variables, then C ?≡sem D always has
a solution.
Proof. Assume that the variable X occurs in C and the variable Y occurs in D,
and let E be an EL concept with rd (E) > k. Let θ be the substitution defined as
θ(X) := θ(Y ) := E and θ(Z) := > for all variables Z in C, D that are different
from X and Y . Then θ(C) ≡ksem ⊥ ≡ksem θ(D). t
u
k
We call a solution σ of C ?≡sem D trivial if σ(C) ≡ksem ⊥ ≡ksem σ(D). The non-
trivial semantically k-restricted unifiers are just the syntactically k-restricted
unifiers. This is an easy consequence of Lemma 2.
Lemma 15. The substitution σ is a non-trivial semantically k-restricted unifier
k k
of C ?≡sem D iff σ is a syntactically k-restricted unifier of C ?≡syn D.
If we view the unification problem in Example 3 as a semantically k-restricted
unification problem, then it does not have a non-trivial solution for k ≤ 2,
but setting σ(X) := σ(Y ) := ∃r.∃r.A yields a trivial solution for k ≤ 2. The
substitution σex is a non-trivial semantically k-restricted unifier of this problem
for all k ≥ 3.
k
Matching problems C ?≡sem D can only have trivial solutions if rd (D) > k.
Restricted Unification in the DL EL 11
k
Lemma 16. Let C ?≡sem D be a matching problem such that rd (D) ≤ k. Then
k k
the set of solutions of C ?≡sem D coincides with the set of solutions of C ?≡syn D.
Using this lemma, it is easy to see that the NP-hardness results shown in the
previous section also hold in the semantically restricted case. We state here only
the general NP-hardness result, but note that the more fine-grained complexity
results given in Propositions 10 and 11 also apply.
Proposition 17. Semantically k-restricted matching is NP-hard.
To show the NP-upper bound for unification, we can proceed as follows for
k
a given semantically k-restricted unification problem C ?≡sem D:
k
1. Check whether C ?≡sem D has a trivial solution. This is the case if the
following holds for all E ∈ {C, D}: E contains a variable or rd (E) > k. If
this test succeeds, then answer “unifiable.” Otherwise, proceed with the next
step.
k
2. If C ?≡sem D does not have a trivial solution, then check whether it has a
k
non-trivial solution by testing whether C ?≡syn D has a solution, using the
NP procedure described in the previous section.
Overall, this yields an NP procedure for testing solvability of semantically k-
restricted unification problems.
Theorem 18. Semantically k-restricted unification in EL is NP-complete.
Unification type zero can be shown by a simple adaptation of the approach
employed above for the syntactically k-restricted case. The proof uses the fact
that, if θ is an instance of σ, then rd (θ(X)) ≥ rd (σ(X)) for all variables occurring
in the unification problem. Consequently, a trivial solution cannot have a non-
trivial solution as an instance.
Theorem 19. Semantically k-restricted EL unification has unification type zero
for any k ≥ 1.
6 Conclusion
We have investigated both a semantically and a syntactically restricted variant
of unification in EL, where either the role depth of concepts or the length of role
paths in interpretations is restricted by a natural number k ≥ 1. In contrast to
the case of FL0 , for EL these restrictions do not lead to an improvement of the
unification type or the complexity of the decision problem. For FL0 , the “bad”
behaviour w.r.t. the unification type and the complexity of the decision problem
depends on the ability to nest value restrictions arbitrarily deep. In contrast,
for EL the “bad” behaviour already shows up for k = 1, where no nesting of
existential restrictions is allowed.
12 F. Baader and M. Rostamigiv
Nevertheless, it may still make sense to consider the syntactically restricted
variant of unification also for EL. In fact, in our experiments with the system
UEL, which implements several unification algorithms for the DL EL [8], we
have observed that the algorithms usually yield many different unifiers, and
it is hard to choose one that is appropriate for the application at hand (e.g.,
when generating new concepts using unification [2]). For this reason, we added
additional constraints to the unification problem to ensure that the generated
concepts are of a similar shape as the concepts already present in the ontology [2].
It makes sense also to use a restriction on the role depth as such an additional
constraint since the role depth of the (unfolded) concepts occurring in real-world
ontologies is usually rather small. This claim is supported by our experiments
with the medical ontology SNOMED CT,2 which has a maximal role depth of
10, and the acyclic ontologies in Bioportal 2017,3 where a large majority also
has a role depth of at most 10. The NP procedure for syntactically k-restricted
unification described in Section 4 is, however, not very useful in this setting since
it basically first computes all local unifiers of the unrestricted problem, and then
throws away the ones that lead to a unified concept whose role depth is too large.
Thus, it would be interesting to find a procedure for syntactically k-restricted
unification in EL that directly generates the local unifiers that are syntactically
k-restricted, without first generating all local unifiers.
Both for FL0 and for EL, decidability of unification in the presence of termi-
nologies (TBoxes) consisting of general concept inclusions is an open problem.
In the restricted setting, decidability should follow from the fact that, up to
equivalence, there can be only finitely many concepts of a bounded role depth if
only finitely many concept names and role names are available. However, for EL
the number of such concepts increase by one exponent with every increase of the
role depth bound. Thus, it would be interesting to see whether an elementary
decision procedure can be obtained for EL in the restricted setting.
Acknowledgements
Franz Baader was partially supported by DFG TRR 248 (cpec, grant 389792660),
and Maryam Rostamigiv by a DAAD Short-Term Grant, 2021 (57552336). The
authors should like to thank Patrick Koopmann for determining the maximal
role depth of concepts in ontologies from Bioportal 2017 and in SNOMED CT.
References
1. Franz Baader, Stefan Borgwardt, and Barbara Morawska. Extending unification
in EL towards general TBoxes. In Proc. of the 13th Int. Conf. on Principles
of Knowledge Representation and Reasoning (KR 2012), pages 568–572. AAAI
Press/The MIT Press, 2012.
2
https://www.snomed.org/
3
https://zenodo.org/record/439510
Restricted Unification in the DL EL 13
2. Franz Baader, Stefan Borgwardt, and Barbara Morawska. Constructing SNOMED
CT concepts via disunification. LTCS-Report 17-07, Chair for Automata The-
ory, Institute for Theoretical Computer Science, Technische Universität Dresden,
Dresden, Germany, 2017. https://lat.inf.tu-dresden.de/research/reports/
2017/BaBM-LTCS-17-07.pdf.
3. Franz Baader, Oliver Fernández Gil, and Maryam Rostamigiv. Restricted unifica-
tion in the description logic FL0 . In Boris Konev and Giles Reger, editors, Proc.
of the 13th International Symposium on Frontiers of Combining Systems (FroCoS
2021), volume 12941 of Lecture Notes in Computer Science. Springer, 2021. To
appear. A long version of this paper containing detailed proofs has been published
as technical report [4].
4. Franz Baader, Oliver Fernández Gil, and Maryam Rostamigiv. Restricted uni-
fication in the DL FL0 (extended version). LTCS-Report 21-02, Chair of Au-
tomata Theory, Institute of Theoretical Computer Science, Technische Universität
Dresden, Dresden, Germany, 2021. https://lat.inf.tu-dresden.de/research/
reports/2021/BaGiRo21.pdf.
5. Franz Baader and Silvio Ghilardi. Unification in modal and description logics. Log.
J. IGPL, 19(6):705–730, 2011.
6. Franz Baader and Ralf Küsters. Matching in description logics with existential re-
strictions. In Proc. of the 7th Int. Conf. on Principles of Knowledge Representation
and Reasoning (KR 2000), pages 261–272, 2000.
7. Franz Baader, Ralf Küsters, and Ralf Molitor. Computing least common subsumers
in description logics with existential restrictions. In Proc. of the 16th Int. Joint
Conf. on Artificial Intelligence (IJCAI’99), pages 96–101, 1999.
8. Franz Baader, Julian Mendez, and Barbara Morawska. UEL: Unification solver
for the description logic EL – system description. In Proc. of the 6th International
Joint Conference on Automated Reasoning (IJCAR 2012), volume 7364 of Lecture
Notes in Artificial Intelligence, pages 45–51. Springer, 2012.
9. Franz Baader and Barbara Morawska. Unification in the description logic EL.
In Ralf Treinen, editor, Proc. of the 20th Int. Conf. on Rewriting Techniques and
Applications (RTA 2009), volume 5595 of Lecture Notes in Computer Science,
pages 350–364. Springer-Verlag, 2009.
10. Franz Baader and Barbara Morawska. SAT encoding of unification in EL. In
C. Fermüller and A. Voronkov, editors, Proc. of the 17th Int. Conf. on Logic for
Programming, Artifical Intelligence, and Reasoning (LPAR-17), volume 6397 of
Lecture Notes in Computer Science, pages 97–111, Yogyakarta (Indonesia), 2010.
Springer-Verlag.
11. Franz Baader and Barbara Morawska. Unification in the description logic EL.
Logical Methods in Computer Science, 6(3), 2010.
12. Franz Baader and Paliath Narendran. Unification of concept terms in description
logics. J. Symbolic Computation, 31(3):277–305, 2001.
13. Franz Baader and Wayne Snyder. Unification theory. In J.A. Robinson and
A. Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–
533. Elsevier Science Publishers, 2001.
14. Philippe Balbiani, Cigdem Gencer, Maryam Rostamigiv, and Tinko Tinchev.
About the unification type of K + ⊥. In Proc. of the 34th International Work-
shop on Unification (UNIF 2020), pages 4:1–4:6. RISC-Linz, 2020.
15. Emil Jerabek. Blending margins: The modal logic K has nullary unification type.
J. Logic and Computation, 25(5):1231–1240, 2015.
16. Ajay Kumar Eeralla and Christopher Lynch. Bounded ACh unification. Math.
Struct. Comput. Sci., 30(6):664–682, 2020.
14 F. Baader and M. Rostamigiv
17. Ralf Küsters. Non-standard Inferences in Description Logics, volume 2100 of Lec-
ture Notes in Artificial Intelligence. Springer-Verlag, 2001.
18. Paliath Narendran. Solving linear equations over polynomial semirings. In Proc.
of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS 1996),
pages 466–472. IEEE Computer Society, 1996.
19. Rafael Peñaloza and Anni-Yasmin Turhan. A practical approach for computing
generalization inferences in EL. In Grigoris Antoniou, Marko Grobelnik, Elena
Paslaru Bontas Simperl, Bijan Parsia, Dimitris Plexousakis, Pieter De Leenheer,
and Jeff Z. Pan, editors, Proc. of the 8th Extended Semantic Web Conference
(ESWC 2011), volume 6643 of Lecture Notes in Computer Science, pages 410–
423. Springer, 2011.