Introduction

Unification theory [13] investigates the unification properties of equational theories (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.

Unification of concept patterns has been proposed as a nonstandard inference service in DL that can, for instance, be used to detect redundancies in ontologies. For example, assume that one ontologist describes the medical concept of myocarditis by the EL concept HeartDisease ∃cause.Virus whereas another one describes it by ViralInfection ∃location.Heart. These two concepts 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 complex concepts. In fact, replacing HeartDisease with Disease ∃location.Heart in the first concept yields Disease ∃location.Heart ∃cause.Virus, and replacing ViralInfection with Disease ∃cause.Virus in the second concept yields Disease ∃cause.Virus ∃location.Heart. These two concepts are clearly equivalent, and they actually yield an appropriate description of myocarditis.

For the DL FL 0 , which has the concept constructors conjunction ( ), value restriction (∀r.C), and top concept ( ), unification was investigated in detail in [12]. It was shown there that unification in FL 0 is ExpTime-complete and of unification type zero. The DL EL, which has the concept constructors conjunction ( ), existential restriction (∃r.C), and top concept ( ), also has unification type zero, but the complexity of the decision problem is lower than for FL 0 : it is "only" NP-complete for EL [11].

In [3], we investigate two kinds of restrictions on unification in FL 0 . 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 FL 0 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 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 FL 0 and EL. Whereas in FL 0 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.

The DL EL and Restrictions

Starting with mutually disjoint countably infinite sets N C and N R of concept and role names, the set of EL concepts is inductively defined as follows: 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.

- (top

Lemma 1 ([11]). Let C = A 1 . . . A k ∃r 1 .C 1 . . . ∃r m .C m and D = B 1 . . . B ∃s 1 .D 1 . . . ∃s n .D n , where A 1 , . . . , A k , B 1 , . . . , B are concept names. Then C D iff {B 1 , . . . , B } ⊆ {A 1 , . . . , A k } and for every j, 1 ≤ j ≤ n, there exists an i, 1 ≤ i ≤ m, such that r i = s j and C i D j .

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 ∈ N C , -rd (C D) = max(rd (C), rd (D)) and rd (∃r.C) = 1 + rd (C).

Using Lemma 1, it is easy to see that C 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 k syn D if C D and rd (C) ≤ k, -C ≡ k syn D if C k syn D and D k syn 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 k syn and ≡ k syn coincide with the classical subsumption and equivalence relations on EL concepts.

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 d 0 , r 1 , d 1 , . . . , d n−1 , r n , d n , where d 0 , . . . , d n are elements of ∆ I , r 1 , . . . , r n are role names, and

(d i−1 , d i ) ∈ r I

i 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 k sem D if C I ⊆ D I holds for all k-restricted interpretations I, -C ≡ k sem D if C k sem D and D k sem 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 ≡ k sem ⊥ iff rd (C) > k, and C ≡ k sem D iff -rd (C) > k and rd (D) > k, or -rd (C) ≤ k, rd (D) ≤ k, and C ≡ D.

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 N V of concept variables, which is disjoint with N C and N R . An EL concept pattern is an EL concept that is constructed using N C ∪ N V 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 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 N V into the set of all EL concept patterns such that dom(σ) := {X ∈ N V | σ(X) = X} is finite. This mapping is extended to concept patterns in the obvious way: 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.

-σ(A) := A for all A ∈ N C ∪ { }, -σ(C D) := σ(C) σ(D)

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 problem X ∃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 ∃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) ≡ and σ(X) ≡ ∃r. .

2.

It then proves that the substitution σ defined as

σ(X) := σ(X) ∃r.Z, σ(Y ) := σ(Y ) Z,

where Z is a new variable, is a unifier of X ∃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 σ is an instance of θ. Since the instance relation is transitive, this implies that σ is an instance of θ. 4. Using the fact that σ(X) ≡ and σ(X) ≡ ∃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. 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: Local substitutions are induced by assignments S, which assign subsets S X 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

O S := {(X, Y ) | X, Y are variables in C or D and Y occurs in S X }

is irreflexive (and thus a partial order). Any acyclic assignment S induces a unique substitution σ S , which can be defined by induction along > S :

-If X is a minimal variable w.r.t. > S , then σ S (X) := E∈S X E.

-Assume that σ S (Y ) is already defined for all Y such that X > S Y . Then σ S (X) := E∈S X σ 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 unification problem C ? ≡ D (and thus can be guessed by an NP procedure), local substitutions may assign exponentially large concepts to a variable. Nevertheless, 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) θ(X) holds for all variables X occurring in C, D, σ θ iff σ θ and θ σ.

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]. Consequently, the instance relation on syntactically k-restricted unifiers (which is defined using ≡ k syn ) 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. Proof. Similarly to the proof of Proposition 4, we consider an arbitrary complete set M of syntactically k-restricted unifiers of X ∃r.Y ? ≡ k syn ∃r.Y . We show that all the steps made in this proof also work in the syntactically k-restricted case.

Syntactically Restricted Unification in EL

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) ≡ and σ(X) ≡ ∃r. . 2. Since σ is a syntactically k-restricted unifier, the same is true for the substitution σ constructed in the second step. In fact, we already know that σ is a unifier, and the concepts ∃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.

This finishes the proof that M cannot be minimal. Since M was chosen as an arbitrary complete set of syntactically k-restricted unifiers of X ∃r.Y ? ≡ k syn ∃r.Y , this shows that this unification problem has unification type zero. 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. 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-restricted unification problem C ? ≡ k 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.

Proof. This can easily be shown by induction along > S , following the inductive definition of the substitution σ S .

It remains to show that this NP procedure is complete, i.e., that it is really the case that any solvable syntactically k-restricted unification problem C ? ≡ k 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 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.

Semantically Restricted Unification in EL

For an integer k ≥ 1, a semantically k-restricted unification problem is an equation of the form C ? ≡ k 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) ≡ k sem σ(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 substitution σ with σ(X) := ∃r.A is a solution if we view this equation as a semantically 1-restricted unification problem. More generally, the following holds. 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 a given semantically k-restricted unification problem C ? ≡ k sem D:

1. Check whether C ? ≡ k 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. 2. If C ? ≡ k sem D does not have a trivial solution, then check whether it has a non-trivial solution by testing whether C ? ≡ k 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 krestricted 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 nontrivial solution as an instance.

Theorem 19. Semantically k-restricted EL unification has unification type zero for any k ≥ 1.

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 FL 0 , for EL these restrictions do not lead to an improvement of the unification type or the complexity of the decision problem. For FL 0 , 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.

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 FL 0 and for EL, decidability of unification in the presence of terminologies (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.