Restricted Unification in the DL E L

Abstract

Research on unification in Description Logic (DL) has concentrated on the lightweight DLs F L0 and EL. For both DLs, the unification type is zero, which is the worst possible type. The complexity of deciding unifiability is ExpTime-complete for F L0 and NP-complete for EL. In a recent paper, we have shown that, for F L0, both the unification type and the complexity of the decision problem can be improved by considering restricted versions of the unification problem where either 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 unification type stays zero, and the complexity of the decision problem stays NP-complete.

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.

Copyright c 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).

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 E L concept HeartDisease u 9cause:Virus whereas another one describes it by ViralInfection u 9location: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 u 9location:Heart in the first concept yields Disease u 9location:Heart u 9cause:Virus ; and replacing ViralInfection with Disease u 9cause:Virus in the second concept yields Disease u 9cause:Virus u 9location:Heart : These two concepts are clearly equivalent, and they actually yield an appropriate description of myocarditis.

For the DL F L0, which has the concept constructors conjunction (u), value restriction (8r:C), and top concept (>), unification was investigated in detail in [ 12 ]. It was shown there that unification in F L0 is ExpTime-complete and of unification type zero. The DL E L, which has the concept constructors conjunction (u), existential restriction (9r:C), and top concept (>), also has unification type zero, but the complexity of the decision problem is lower than for F L0: it is “only” NP-complete for E L [ 11 ].

In [ 3 ], we investigate two kinds of restrictions on unification in F L0. 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 F L0 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 E L. 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 F L0 and EL. Whereas in F L0 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 E L 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 2 NC is an EL concept, – if C, D are EL concepts and r 2 NR is a role name, then C uD (conjunction) and 9r:C (existential restriction) are EL concepts. follows: 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 >I = I and (C u D)I = CI \ DI; (9r:C)I = fx 2 I j 9y 2 I: (x; y) 2 rI ^ y 2 CIg: Given two EL concepts C and D, we say that C is subsumed by D (written C v D) if CI 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 9r1:C1 u : : : u 9rm:Cm and D = B1 u : : : u B` u 9s1:D1 u : : : u 9sn:Dn, where A1; : : : ; Ak; B1; : : : ; B` are concept names. Then C v D iff fB1; : : : ; B`g fA1; : : : ; Akg 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 2 NC , – rd (C u D) = max(rd (C); rd (D)) and rd (9r:C) = 1 + rd (C). Using Lemma 1, it is easy to see that C v D implies rd (C) rd (D). Thus, the role depth of E L concepts is preserved under equivalence.

We are now ready to define our first restricted version of subsumption and equivalence in E L. For an integer k 1 and E L concepts C and D, we define subsumption and equivalence restricted to concepts of role depth k as follows: – C vskyn D if C v D and rd (C) k, – C skyn D if C vskyn D and D vskyn 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 vskyn and skyn coincide with the classical subsumption and equivalence relations on E L 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) 2 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 E L concepts C and D, we define subsumption and equivalence restricted to interpretations with role paths of length k as follows: – C vskem D if CI DI holds for all k-restricted interpretations I, – C skem D if C vskem D and D vskem 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 E L concept such that rd (C) > k, then CI = ;. The following lemma is an easy consequence of this fact, where ? denotes the bottom concept, which is interpreted as ?I = ; in every interpretation I.

1 and C; D be E L concepts. Then C k sem ? iff rd (C) > k,

Lemma 2. Let k

and C skem D iff – rd (C) > k and rd (D) > k, or – rd (C) k, rd (D) k, and C 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 E L concept pattern is an E L 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 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 E L concept patterns such that dom( ) := fX 2 NV j (X) 6= Xg is finite. This mapping is extended to concept patterns in the obvious way: – – (A) := A for all A 2 NC [ f>g, (C u D) := (C) u (D) and (9r:C) := 9r: (C).

An E L unification problem is an equation of the form C ? D where C; D are E L concept patterns. A unifier (or solution) of this equation is a substitution such that (C) (D).

Example 3. Consider the E L unification problem 9r:X u 9s:9r:A ? 9r:9s:Y u 9s:Y: It is easy to see that (up to equivalence and restricted to the variables X; Y ) the substitution ex with dom( ex ) = fX; Y g, ex (X) = 9s:9r:A, and ex (Y ) = 9r: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 E L 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 E L has unification type zero means that there is an E L unification problem that has type zero. Thus, the following proposition implies that E L indeed has unification type zero.

Proposition 4 ([ 11 ]). Let X; Y be concept variables. The E L unification problem X u 9r:Y ? 9r: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 9r:Y ? 9r:Y is non-minimal, proceeds as follows: 1. It observes that the substitution with (X) = 9r: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 9r:>. 2. It then proves that the substitution b defined as b(X) := (X) u 9r:Z; b(Y ) := (Y ) u Z;

where Z is a new variable, is a unifier of X u 9r:Y ? 9r: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 9r:>, 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 E L unification 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. NPhardness 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 reductions with different characteristics: (R1) In [ 6 ], a given propositional formula is translated into an E L 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 E L 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 E L could be proved in [ 9,11 ].

Theorem 5 ([ 9,11 ]). Unification in E L is NP-complete.

Showing the NP-upper bound for unification in E L 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 E L 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. To be more precise, it is shown in [ 9,11,1 ] that a given E L 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 9r: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 := f(X; Y ) j X; Y are variables in C or D and Y occurs in SX g 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) := dE2SX E. – Assume that S (Y ) is already defined for all Y such that X >S Y . Then

S (X) := dE2SX 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 E L 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:

6 iff (X) v (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 E L 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 E L unification problem has a local unifier that does not use minimal unifiers can be found in [ 1 ]. 4

Syntactically Restricted Unification in E L

For an integer k 1, a syntactically k-restricted unification problem is an equation of the form C ? k

syn D, where C; D are E L concept patterns. A unifier of this equation (also called syntactically k-restricted unifier ) is a substitution such that (C) skyn (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 substitution 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 skyn and the fact that rd ( (X)) rd ( (D)) for every substitution and every concept variable X occurring in the E L concept D.

Lemma 6. If

unifier of C ? C or D.

is a syntactically k-restricted unifier of C ? skyn D, then is a

D and rd ( (X)) k for every concept variable X occurring in Consequently, the instance relation on syntactically k-restricted unifiers (which is defined using skyn ) 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 E L unification problem X u9r:Y ? skyn 9r:Y has unification type zero for every k 1. Proof. Similarly to the proof of Proposition 4, we consider an arbitrary complete set M of syntactically k-restricted unifiers of X u 9r:Y ? k syn 9r:Y . We show that all the steps made in this proof also work in the syntactically k-restricted case. 1. The unifier with (X) = 9r: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 2 M .

As before, we conclude that satisfies (X) 6 > and (X) 6 9r:>. 2. Since is a syntactically k-restricted unifier, the same is true for the substitution b constructed in the second step. In fact, we already know that b is a unifier, and the concepts b(X u 9r:Y ) = (X) u 9r:Z u 9r:( (Y ) u Z) and b(9r:Y ) = 9r:( (Y ) u Z) have role depth 1 since is a syntactically k-restricted unifier of Xu9r:Y ? k syn 9r: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 2 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. 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 u9r:Y ? k syn 9r:Y , this shows that this unification problem has unification type zero. tu Theorem 8. Syntactically k-restricted E L 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.

Lemma 9. Let C ? k

syn D be a syntactically k-restricted E L matching problem. 1. If rd (D) > k, then C ? k

syn D does not have a solution. 2. Otherwise, a substitution

D iff it is a matcher of C ? is a syntactically k-restricted matcher of C ? k syn

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-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 . tu

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 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 E L is NP-complete. 5

Semantically Restricted Unification in E L

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 E L concept patterns. A unifier of this equation (also called semantically k-restricted unifier ) is a substitution such that (C) skem (D).

In contrast to the syntactic case, solvability in the semantically k-restricted setting does not imply solvability in the unrestricted setting. For example, 9r:X? 9s:X for distinct role names r; s clearly does not have a solution, but the substitution with (X) := 9r:A is a solution if we view this equation as a semantically 1-restricted unification problem. More generally, the following holds. Lemma 14. If C; D both contain concept variables, then C ? k 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 E L 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) skem ? skem (D). tu

We call a solution of C ? skem D trivial if (C) skem ? skem (D). The nontrivial 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 of C ? skem D iff is a syntactically k-restricted unifier of C ? skyn 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 ) := 9r:9r: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.

Matching problems C ? k sem D can only have trivial solutions if rd (D) > k. Lemma 16. Let C ? skem D be a matching problem such that rd (D) k. Then the set of solutions of C ? k syn D.

sem D coincides with the set of solutions of C ? k

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 2 fC; Dg: 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 E L 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 E L 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 E L, 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 F L0, for E L these restrictions do not lead to an improvement of the unification type or the complexity of the decision problem. For F L0, 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 E L 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 E L. In fact, in our experiments with the system UEL, which implements several unification algorithms for the DL E L [ 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 E L that directly generates the local unifiers that are syntactically k-restricted, without first generating all local unifiers.

Both for F L0 and for E L, 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 E L 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 E L 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. 2 https://www.snomed.org/ 3 https://zenodo.org/record/439510

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. Franz Baader , Stefan Borgwardt, and Barbara Morawska . Constructing SNOMED CT concepts via disunification . LTCS-Report 17-07 , Chair for Automata Theory, 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 unification in the description logic F L0 . 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 unification in the DL F L0 (extended version) . LTCS-Report 21-02 , Chair of Automata 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 restrictions . 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 Workshop 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 .

17. Ralf Küsters . Non-standard Inferences in Description Logics , volume 2100 of Lecture 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 .