Unification in DLs has been proposed in [7] (for the DL F L0, which offers the constructors conjunction (u), value restriction (8r:C), and the top concept (>)) as a novel inference service that can, for instance, be used to detect redundancies in ontologies. For example, assume that one developer of a medical ontology defines the concept of a patient with severe head injury as Patient u 9 nding:(Head_injury u 9severity:Severe); whereas another one represents it as Patient u 9 nding:(Severe_ nding u Injury u 9 nding_site:Head): These two concept descriptions are not equivalent, but they are nevertheless meant to represent the same concept. They can obviously be made equivalent by treating the concept names Head_injury and Severe_ nding as variables, and substituting the first one by Injury u 9 nding_site:Head and the second one by 9severity:Severe. In this case, we say that the descriptions are unifiable, and call the substitution that makes them equivalent a unifier. Intuitively, such a unifier proposes definitions for the concept names that are used as variables: in our example, we know that, if we define Head_injury as Injury u 9 nding_site:Head and Severe_ nding as 9severity:Severe, then the two concept descriptions (1) and (2) are equivalent w.r.t. these definitions. Here equivalence holds without additional GCIs. To motivate our interest in unification w.r.t. GCIs, assume that the second developer uses the description
(1) (2)
(3)
instead of (2). The descriptions (1) and (3) are not unifiable without additional
? Supported by DFG under grant BA 1122/14-1 is present in a background ontology.
In [
[
E L w.r.t. cycle-restricted general TBoxes, which extends the one from [
The Description Logic E L
Syntax and semantics of E L are defined in the usual way (see, e.g., [
A general concept inclusion (GCI) is of the form C v D for concept
descriptions C; D, and a general TBox is a finite set of GCIs. An interpretation I
satisfies such a GCI if CI DI , and it is a model of the general TBox T if it
satisfies all GCIs in T . Subsumption asks whether a given GCI C v D follows
from a general TBox T , i.e. whether every model of T satisfies C v D. In this
case we say C is subsumed by D w.r.t. T and write C vT D. Subsumption in
E L w.r.t. a general TBox is known to be decidable in polynomial time [
An E L-concept description is an atom if it is an existential restriction or a concept name. The atoms of an E L-concept description C are the subdescriptions of C that are atoms, and the top-level atoms of C are the atoms occurring in the top-level conjunction of C. Obviously, any E L-concept description is the conjunction of its top-level atoms, where the empty conjunction corresponds to >. The atoms of a general TBox T are the atoms of all the concept descriptions occurring in T .
structure is compatible. To be more precise, we define structural subsumption
between atoms as follows: the atom C is structurally subsumed by the atom D
w.r.t. T (C vsT D) iff either (i) C = D is a concept name, or (ii) C = 9r:C0,
D = 9r:D0, and C0 vT D0. It is easy to see that subsumption w.r.t. ; between
two atoms implies structural subsumption w.r.t. T , which in turn implies
subsumption w.r.t. T . The unification algorithm in [
for subsumption w.r.t. a general TBox, which is similar to the one developed in
[
Definition 2. The general TBox T is called cycle-restricted iff there is no nonempty word w 2 NR+ and E L-concept description C such that C vT 9w:C.
restrictedness. The main idea is that it is sufficient to consider the cases where C is a concept name or >.
Lemma 3. Let T be a general TBox. It can be decided in time polynomial in the size of T whether T is cycle-restricted or not. 3
Unification in E L w.r.t. General TBoxes
replaced by substitutions) and a set Nc of concept constants (which must not be replaced by substitutions). A substitution maps every concept variable to an E L-concept description. It is extended to concept descriptions in the usual way: – – (A) := A for all A 2 Nc [ f>g, (C u D) := (C) u (D) and
(9r:C) := 9r: (C).
An E L-concept description C is ground if it does not contain variables. Obviously, a ground concept description is not modified by applying a substitution.
Definition 4. Let T be a general TBox that is ground. An E L-unification problem w.r.t. T is a finite set = fC1 v? D1; : : : ; Cn v? Dng of subsumptions between E L-concept descriptions. A substitution is a unifier of w.r.t. T if solves all the subsumptions in , i.e. if (C1) vT (D1); : : : ; (Cn) vT (Dn). We say that is unifiable w.r.t. T if it has a unifier.
Note that we have restricted the background general TBox T to be ground.
This is not without loss of generality. If T contained variables, then we would
need to apply the substitution also to its GCIs, and instead of requiring (Ci) vT
(Di) we would thus need to require (Ci) v (T ) (Di), which would change
the nature of the problem considerably (see [
first normalize the TBox and the unification problem appropriately. An atom is called flat if it is a concept name or an existential restriction of the form 9r:A for a concept name A. The general TBox T is called flat if it contains only GCIs of the form A u B v C, where A; B are flat atoms or > and C is a flat atom.
the form C1 u u Cn v? D, where n 0 and C1; : : : ; Cn; D are flat atoms.1
Let be a unification problem and T a general TBox. By introducing
auxiliary variables and concept names, respectively, and T can be transformed in
polynomial time into a flat unification problem 0 and a flat general TBox T 0
such that the unifiability status remains unchanged, i.e., has a unifier w.r.t.
T iff 0 has a unifier w.r.t. T 0. In addition, if T was cycle-restricted, then so is
T 0 (see [
that any E L-unification problem that is unifiable has a so-called local unifier. Let T be a flat cycle-restricted TBox and a flat unification problem. The atoms of are the atoms of all the concept descriptions occurring in . We define Atnv := At n Nv
At := fC j C is an atom of T or of (non-variable atoms).
g and
f(X; Y ) 2 Nv
Nv j Y occurs in an element of SX g: 1 If n = 0, then we have an empty conjunction on the left-hand side, which as usual stands for >.
order). Any acyclic assignment S induces a unique substitution S , which can be defined by induction along >S : – If X 2 Nv is minimal w.r.t. >S , then we define S (X) := d – Assume that (Y ) is already defined for all Y such that X >D2SSYX .DT. hen we define S (X) := dD2SX S (D):
ment S such that = S . If the unifier of w.r.t. T is a local substitution, then we call it a local unifier of w.r.t. T .
The main technical result shown in [
The brute-force algorithm is not practical since it blindly guesses an acyclic
assignment and only afterwards checks whether the guessed assignment induces
a unifier. We now introduce a more goal-oriented unification algorithm, in which
nondeterministic decisions are only made if they are triggered by “unsolved parts”
of the unification problem. In addition, failure due to wrong guesses can be
detected early. Any non-failing run of the algorithm produces a unifier, i.e.,
there is no need for checking whether the assignment computed by this run
really produces a unifier. This goal-oriented algorithm generalizes the algorithm
for unification in E L w.r.t. the empty TBox introduced in [
We assume without loss of generality that the cycle-restricted TBox T and the unification problem 0 are flat. Given T and 0, the sets At and Atnv are defined as above. Starting with 0, the algorithm maintains a current unification problem and a current acyclic assignment S, which initially assigns the empty set to all variables. In addition, for each subsumption in it maintains the information on whether it is solved or not. Initially, all subsumptions are unsolved, except those with a variable on the right-hand side. Rules are applied only to unsolved subsumptions. A (non-failing) rule application does the following: – it solves exactly one unsolved subsumption, – it may extend the current assignment S, and – it may introduce new flat subsumptions built from elements of At.
every subsumption s 2 of the form C1 u u Cn v? X is expanded by adding the subsumption C1 u u Cn v? A to for every A 2 SX .
Eager Ground Solving: Eager Solving:
Condition: This rule applies to s = C1 u u Cn v? D if it is ground. Action: If C1 u u Cn vT D does not hold, the rule application fails. Otherwise, s is marked as solved.
Condition: This rule applies to s = C1 u u Cn v? D if either – there is i 2 f1; : : : ; ng such that Ci = D or Ci = X 2 Nv and D 2 SX , or – D is ground and d G vT D holds, where G is the set of all ground atoms in fC1; : : : ; Cng [ SX2fC1;:::;Cng\Nv SX .
Action: Its application marks s as solved.
Eager Extension:
Condition: This rule applies to s = C1 u uCn v? D if there is i 2 f1; : : : ; ng with Ci = X 2 Nv and fC1; : : : ; Cng n fXg SX .
Action: Its application adds D to SX . If this makes S cyclic, the rule application fails. Otherwise, is expanded w.r.t. X and s is marked as solved.
subsumption is added to , either by a rule application or by expansion of , then it is initially designated unsolved, except if it has a variable on the righthand side. Once a subsumption is in , it will not be removed. Likewise, if a subsumption in is marked as solved, then it will not become unsolved later.
solved by the substitution induced by the current assignment. It may be the case that the task of satisfying the subsumption was deferred to solving other subsumptions which are “smaller” than the given subsumption in a well-defined sense. The task of solving a subsumption whose right-hand side is a variable is deferred to solving the subsumptions introduced by expansion.
Algorithm 5. Let 0 be a flat E L-unification problem. We set := 0 and SX := ; for all X 2 Nv. While contains an unsolved subsumption, apply the steps (1) and (2). Once all subsumptions are solved, return the substitution induced by the current assignment. (1) Eager rule application: If some eager rules apply to an unsolved subsumption s in , apply one of highest priority. If the rule application fails, then return “not unifiable”. (2) Nondeterministic rule application: If no eager rule is applicable, let s be an unsolved subsumption in . If one of the nondeterministic rules applies to s, nondeterministically choose one of these rules and apply it. If none of these rules apply to s or the rule application fails, then return “not unifiable”.
Condition: This rule applies to s = C1 u u Cn v? 9s:D0 if there is at least one index i 2 f1; : : : ; ng with Ci = 9s:C0.
Action: Its application chooses such an index i, adds the subsumption C0 v? D0 to , expands it w.r.t. D0 if D0 is a variable, and marks s as solved. Extension:
Condition: This rule applies to s = C1 u u Cn v? D if there is at least one i 2 f1; : : : ; ng with Ci 2 Nv.
Action: Its application chooses such an i and adds D to SCi . If this makes S cyclic, the rule application fails. Otherwise, is expanded w.r.t. Ci and s is marked as solved.
care nondeterministic. However, choosing which rule to apply to the chosen subsumption is don’t know nondeterministic. Additionally, the application of nondeterministic rules requires don’t know nondeterministic guessing.
The eager rules are mainly there for optimization purposes, i.e., to avoid
nondeterministic choices if a deterministic decision can be made. For example,
a ground subsumption, as considered in the Eager Ground Solving rule, either
follows from the TBox, in which case any substitution solves it, or it does not,
in which case it does not have a solution. This condition can be checked in
polynomial time using the polynomial time subsumption algorithm for E L [
The nondeterministic rules only come into play if no eager rules can be applied. In order to solve an unsolved subsumption s = C1 u u Cn v? D, we consider the two conditions of Lemma 1. Regarding the first condition, which is addressed by the rules Decomposition and Extension, assume that is induced by an acyclic assignment S. To satisfy the first condition of the lemma with , the atom (D) must subsume a top-level atom in (C1) u u (Cn). This atom can either be of the form (Ci) for an atom Ci, or it can be of the form (C) for an atom C 2 SCi and a variable Ci. In the second case, the atom C can either already be in SCi or it can be put into SCi by an application of the Extension rule.
Mutation 1:
Condition: This rule applies to s = C1 u u Cn v? D if n > 1 and there are atoms A1; : : : ; Ak; B of T such that A1 u u Ak vT B holds.
Action: Its application chooses such atoms, marks s as solved, and generates the following subsumptions: – it chooses for each 2 f1; : : : ; kg an i 2 f1; : : : ; ng and adds the new subsumption Ci v? A to , – it adds B v? D to .
Mutation 2:
Condition: This rule applies to s = 9r:X v? D if X is a variable, D is ground, and there are atoms 9r:A1; : : : ; 9r:Ak of T such that 9r:A1 u u 9r:Ak vT D holds.
Action: Its application chooses such atoms, adds A1; : : : ; Ak to SX , expands w.r.t. X, and marks s as solved.
Mutation 3:
Condition: This rule applies to s = 9r:X v? 9s:Y if X and Y are variables, and there are atoms 9r:A1; : : : ; 9r:Ak; 9s:B of T with 9r:A1 u u 9r:Ak vT 9s:B.
Action: Its application chooses such atoms, marks s as solved, and generates the following subsumptions: – it adds A1; : : : ; Ak to SX and expands w.r.t. X, – it adds the subsumption B v? Y to and expands it w.r.t. Y .
Mutation 4:
Condition: This rule applies to s = C v? 9s:Y if C is a ground atom or >, Y is a variable, and there is an atom 9s:B of T such that C vT 9s:B holds. Action: Its application chooses such an atom, adds the new subsumption B v? Y to , expands this subsumption w.r.t. Y , and marks s as solved. subsumption (E) vsT (F ) to hold for a (hypothetical) unifier of , the rule creates the new subsumption E v? F , which has to be solved later on. This way, the rule ensures that the substitution built by the algorithm actually satisfies the conditions of the lemma. To check the subsumption A1 u u Ak vT B, the rule again employs a polynomial-time subsumption algorithm.
Soundness We will show that, if Algorithm 5 returns a substitution on input
0, then is a unifier of 0 w.r.t. T . In the following, let S be the final acyclic
assignment computed by a non-failing run of Algorithm 5 on input 0, and
the substitution induced by S. By b we denote the final set of subsumptions
computed by this run, i.e., the original subsumptions of 0 together with the
new ones generated by rule applications. To show that solves all subsumptions
in b, we use well-founded induction [
– s is small if n = 1 and C1 is ground or Cn+1 is ground. – We define m(s) := (m1(s); m2(s); m3(s)), where m1(s) := 0 if s is small, and m1(s) := 1 otherwise; m2(s) := X if Cn+1 = X or Cn+1 = 9r:X for a variable X and some r 2 NR, and m2(s) := ? otherwise; m3(s) := maxfrd( (Ci)) j i 2 f1; : : : ; n + 1gg where rd yields the role depth of a concept description, i.e., the maximal nesting of existential restrictions. – The strict partial order on such triples is the lexicographic order, where the first and the third component are compared w.r.t. the normal order > on natural numbers. The variables in the second component are compared w.r.t. the relation >S induced by S, and ? is smaller than any variable. – We extend to b by setting s1 s2 iff m(s1) m(s2).
well-founded [
Lemma 7.
is an E L-unifier of b w.r.t. T , and thus also of its subset 0.
Proof. Let s 2 b and assume that solves all subsumptions s0 2 b with s0 s.
– If s has a non-variable atom as its right-hand side, then it was initially
marked as unsolved and must have been marked solved by a successful rule
application. As an example, we consider the application of the Decomposition
rule (the other rules can be treated similarly [
Observe first that m2(s) = m2(s0) since either 9s:D0 and D0 contain the same variable or are both ground. We now make a case distinction based on m1(s0). If s0 is small, then s is either non-small, i.e. m1(s) > m1(s0), or small and of the form 9s:C0 v? 9s:D0. In the second case, we have m1(s) = m1(s0) and m3(s) > m3(s0). If s0 is non-small, then both C0 and D0 are variables, and thus s is also non-small, which yields m1(s) = m1(s0). Furthermore, the maximal role depth obviously decreases when going from s to s0, and thus m3(s) > m3(s0). In all cases we have shown m(s) m(s0), i.e., s s0. – If s has a variable as its right-hand side, it is of the form C1 u u Cn v? X and for every A 2 SX there is a subsumption sA = C1 u u Cn v? A in b. If s is small, then n = 1 and C1 is ground, and thus the subsumptions sA are also small. Thus, we have m1(s) m1(sA) for every A 2 SX . Furthermore, we have m2(s) > m2(sA) since A is ground or contains a variable on which X depends. This yields s sA, and thus by induction (C1)u u (Cn) vT (A) for every A 2 SX , which implies that (C1) u u (Cn) vT (X) by the definition of . Completeness Assume that 0 is unifiable w.r.t. T and let be a ground unifier of 0 w.r.t. T . We use this unifier to guide the application of the nondeterministic rules such that Algorithm 5 does not fail. The following invariants for and S will be maintained: (I) is a unifier of . (II) For all B 2 SX we have (X) vT (B).
Since SX is initialized to ; for all variables X 2 Nv and is initialized to 0, these invariants are satisfied after the initialization of the algorithm.
namely that the current assignment becomes cyclic. This is the only place in the whole proof where our assumption on cycle-restrictedness of T is needed. Lemma 8. If invariant (II) is satisfied, then the current assignment S is acyclic.
Lemma 9. Assume that the current set of subsumptions signment S satisfy the invariants (I) and (II), and let s 2 and the current asbe unsolved. 1. If an eager rule applies to s, then its application does not fail and the resulting set 0 and assignment S0 also satisfy the invariants (I) and (II). 2. If no eager rule applies to s, then there is a nondeterministic rule that can successfully be applied to s such that the resulting set 0 and assignment S0 also satisfy the invariants (I) and (II).
is a non-failing run of Algorithm 5 on 0 during which the invariants (I) and (II) are satisfied. Together with the fact that every run of the algorithm terminates (see below), this shows completeness, i.e., whenever 0 has a unifier w.r.t. T , the algorithm computes one.
sumption encountered during this run falls into one of the following categories:
2. subsumptions created by expansion from 0: these are of the form C1 u
Cn v? A for a subsumption C1 u u Cn v? X 2 0 and A 2 Atnv; 3. subsumptions of the form C v? D for C; D 2 At. u Since the cardinality of At is polynomially bounded by the size of 0 and T , there are only polynomially many subsumptions of this form. Rules are only applicable to subsumptions that are marked unsolved, and the application of a rule marks at least one subsumption as solved. Thus, only polynomially many rules can be applied during the run. In addition, each rule application takes only polynomial time. This shows that every run of the algorithm terminates in polynomial time.
Theorem 10. Algorithm 5 is an NP-decision procedure for unifiability in E L w.r.t. cycle-restricted TBoxes.
We have presented a goal-oriented NP-algorithm for unification in E L w.r.t.
cycle-restricted TBoxes. In [
unification w.r.t. unrestricted general TBoxes. In order to generalize the bruteforce algorithm in this direction, we need to find a more general notion of locality.