The paper presents a proof that the uni cation in the description logic F L? is decidable in ExpTime. F L? adds to the constructors of the description logic F L0, bottom (inconsistency) which allows us to express a kind of negation. The result is obtained by a careful elimination of ? ( attening) from a given uni cation problem and solving the remaining problem with the F L0-uni cation procedure, which was presented in our previous papers.
F L? is a small description logic which extends the description logic F L0 with a concept expressing inconsistency, ? (bottom). Hence it is a description logic in ? Copyright ' 2020 for the paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). which one can express the concepts constructed over a nite set of concept names N and binary predicate symbols (roles) R, with conjunction, u, top constructor >, value restriction 8r:C, where C is an already formed concept, and ?, bottom. Hence the concepts of F L? may be seen as generated by the following grammar:
C 7! A j >j ? j C u C j 8r:C where A 2 N and r 2 R. The F L? concepts are interpreted as subsets of a non-empty domain, and role names as binary relations between elements of this domain. The universal value restriction 8r:C is then interpreted as a subset of elements of the domain such that, they are related by r with only elements in the interpretation of C.
One of the basic questions about the concepts in F L? is what subsumption relations occur between them. A subsumption holds between C and D, C v D, if an interpretation of C is a subset of an interpretation of D in any domain, in any interpretation of concept names and role names. We de ne equivalence as two subsumptions C D i C v D and D v C.
Since we have only universal role restrictions of the form 8r:C in F L?, 8r may be distributed over conjunction. Hence 8r behaves as a homomorphism: 8r:(C1 u Cn) 8r:C1 u 8r:C2.
A concept of the form 8r1:8r2: : : : 8rm:A (in short 8r1r2 : : : rm:A) is called a particle. In a particle 8r1r2 : : : rm:A a sequence of roles r1 : : : rm is called a role string and it may be empty. A particle: 8r1r2 : : : rm:A where A is a concept name is called an A-particle. A particle: 8r1r2 : : : rm:? is called a ?-particle. A particle: 8r1r2 : : : rm:> is called a >-particle. Each >-particle reduces to >.
Throughout the paper we will use implicitly the following equivalences as left-to-right reducing rules: C u > C; C u ? ?; 8v:(C1 u C2) 8v:C1 u 8v:C2; where C; C1; C2 are any F L? concepts. The following basic properties of subsumption in F L? are also used without proof: 8v:> > and ? v C; C v >; 8v1:? v 8v2:? if the role string v1 is a pre x of v2.
A concept C is in a normal form i C is a conjunction of particles. Hence we view a concept C as a set of particles and use notation C = fP1; P2; : : : ; Png. In this perspective > is treated as the empty conjunction or the empty set of particles. Dually, ? may be understood as an in nite set of all particles, but we rather treat it as a special concept name interpreted always by an empty subset of an interpretation domain.
It is a common knowledge that the subsumption problem in F L? is polynomial, e.g. [5, p. 81]. A simple procedure adapted to our normal form can be found in Appendix A.
If C v P holds, where P is a particle, then P 2 C or there is a ?-particle P 0 2 C such that P 0 v P . For each subsumption C v? D that holds in F L? and for every particle P 2 D we choose P 0 2 C, such that P 0 v P and set that P 0; P are in solving relation, P 0 P .1 1 There may be a choice of particles in C, but we can choose arbitrary. Example 1. Consider a subsumption 8sr:? u 8rrs:A v 8srs:A. Here we can decide that the particle P = 8srs:A is solved by P 0 = 8sr:?, 8sr:? 8srs:A. 3
In order to de ne uni cation, we have to assume a set of concept names Var (variables), disjoint from N (constants) and allow the variables to be substituted by F L? concepts. Hence now we assume that the F L? concepts are constructed over the set of constants and variables. If a concept does not contain variables, we call it ground.
Uni cation problem is de ned as a set of goal subsumptions between F L? concepts in normal form: = fC1 v? D1; : : : ; Cn v? Dng:
Each of the goal subsumptions contains concepts in normal form, and without loss of generality we can assume that each Di is a particle. We call the particles in , goal particles.
We de ne a solution or uni er for the uni cation problem as an assignment of ground concepts to variables such that the goal subsumptions hold. If is such an assignment, by [P ! P 0] we mean replacement of the particle P by P 0 everywhere in the range of . If a variable is assigned by a solution an empty conjunction of particles, we understand that it is substituted by the top constructor, >. The variables substituted with ? will be called ?-variables, and the variables substituted with >, >-variables.2
Since in ( ) all subsumptions hold, we can identify a solving relation ( ) between ground particles in these subsumptions under . Since there may be some choice in de ning a solving relation for ( ), from now on we assume that one such choice was made and the relation is de ned.
A solving relation between the ground particles may not be visible in the goal subsumptions, because di erent particles in the substitution for one goal particle may be solved by the substitution of di erent goal particles, as in the following example.3 Example 2. Let the goal subsumption be: 8rs:Z u8r:Y v? 8rsr:X. If the solution is: = [Z 7! rr:?; Y 7! 8srs:?; X 7! f8r:?; 8s:?g]. Neither (8rs:Z) nor (8r:Y ) is subsumed separately by (8rsr:X).
The idea of a uni cation procedure which we are going to see, is to reduce a uni cation problem to a problem that can be solved by a F L0-uni cation procedure. The lemmas in the following subsections show the properties of F L? uni ers that will be used to justify such a reduction. 2 Notice that these concepts of ?- or >-variables make sense only relative to a solution. 3 This is the important di erence between EL and FL?. 3.1
Removing redundant particles
In Lemma 1 we observe that one can always remove redundant particles from
the range of a uni er. This process is similar to the one we used for obtaining
minimal E L uni ers w.r.t. the inverse of subsumption in [
De nition 1. Let be a uni cation problem, X a goal variable and a solution. A particle P in (X) will be called redundant in (X) if there is no particle P 0 in ( ), such that P solves P 0.
Lemma 1. Let be a uni cation problem and its solution. Let P be a redundant particle in (X). Then a substitution 0, which is like with all P 2 (X) replaced by > is still a uni er.
Proof. The claim follows from the properties of the F L? subsumption. If P is redundant in (X), there is no particle which is solved by the occurrence of P in (X). Hence if P is replaced by >, then no subsumption of the form P v P 0 which holds before the replacement is broken. Now if P 0 v P before the replacement, then it holds after the replacement too, because P 0 v > by the properties of the F L? subsumption. An example of this process may be found in Appendix B, Example 4. 3.2
Cycles We can eliminate redundant ?-particles as well as any other redundant particles in this way. Removing all ? symbols from the range of may not be possible for two reasons.
{ A cyclic solving relation between particles (De nition 2) { A ?-particle that is used in solving a ground goal particle.
In order to formalize the notion of cycle, we give the following de nition. De nition 2. Let be a solution for a uni cation problem
.
1, 8vj :uj :? 1. A path of ?-particles in ( ) is a sequence of ?-particles: 8v1:u1:?; : : : ; 8vk:uk:? such that: (a) Each 8ui:? is in (Xi). (b) For odd j, 1 j k 8vj+1:uj+1:?, Xj+1 = Xj+2 and 8uj+1:? = 8uj+2:?
We denote such a path by: 8v1:u1:? + 8vk:uk:?. 2. Two paths P1; P2 intersect with each other if there is a ?-particle 8u:? 2 (X) such that 8v:u:? 2 8v: (X) is in P1, and 8v0:u:? 2 8v0: (X) is in P2. 3. A cycle in ( ) is a set of paths in ( ) such that each path intersects with at least one of the other paths in the set and there is at least one path in the set 8vi:ui:?; : : : ; 8vi+l:ui+l:? such that Xi = Xi+l and 8ui:? = 8ui+l:?. For a simple example illustrating this de nition look at Example 5.
Even if a uni cation problem has no goal ?-particles, it may not have a solution without ?. This is illustrated by the following example.
Example 3. = fX v? A; X v? 8r:Y; Y v? 8r:Xg
It is easy to see that X cannot be solved by >. A solution for X may contain A or be ?. The two next subsumptions create a cycle, which can be solved either by > or ?-particles. Hence X has to be ? and then Y has to be ? or contain 8r:?. 3.3
We cannot remove all ?-particles from the solution of a uni cation problem, but we can reduce their height.
Lemma 2. Let be a uni cation problem, is a solution. Then there is a unier 0, that is the same as , except that for each ?-particle 8v:u:? in 0(8v:X), there is a ?-variable 0(Y ) = ? such that 0(8v0:Y ) + 8v:u:?.
Proof. Let the ?-particles in ( ) be: 8v1u1:?; 8v2u2:?; : : : ; 8vnun:?. These ?-particles are in substitution for the goal particles: 8v1:X1; 8v2:X2; : : : ; 8vn:Xn.
In order to minimize the role strings of these particles we cannot change vi's, because these role strings come from . We construct 0 by modifying su xes ui of the role strings in the ?-particles in the range of .
Step 1. Remove u from every ?-particle 8u:? in (X) for every goal variable X that contains a ?-particle. Now all variables with ?-particles become ?variables if the reduction to ? is applied. In fact, we postpone performing such reduction till the end, in order to keep all solving relations from de ned (even if they do not hold after the replacement).
Notice that for every particle P such that (X) v P , the subsumption is preserved in 0, 0(X) = ? v P , but the solving relation between ?-particles may be broken in many places. For example take the subsumption: 8vi: (X) v (Y ) where (Y ) = f8vj :?g, now after substituting X and Y with ?, 8vi:? 6v ?.
All solving subsumptions of the form 0(8vi:Xi) v 0(8vj :Xj ), where vi is a pre x of vj hold in 0. The only solving relations that are broken are those where vj is a proper pre x of vi. One of these possibilities must occur, since is a uni er.4
Step 2. In this step we repair the solving relation of in all places that it is broken in 0. We keep the following invariants: 1. If 8vi:u0i:? is in 0(8vi:Xi), then viu0i is a pre x (not necessarily proper) of viui, where 8vi:ui:? 2 (8vi:Xi).
Obviously, this is true before Step 2. Keeping this invariant ensures that the process of repairing the solving relation will terminate, because at worst we will recover the substitution in this way, and then all solving relations hold. 2. The second invariant is the part of the claim in the lemma: for each ?-particle 8v:u:? in 0(8v:X), there is a ?-variable 0(Y ) = ? such that 0(8v0:Y ) + 8v:u:?. Y is then called an anchor variable. 4 Either vi is a pre x (not necessarily proper) of vj or vj is a proper pre x of vi.
The following process is to be performed exhaustively.
Assume: { 8viui:? 2 (Xi), 8vj :uj :? 2 (Xj ), { there is the solving relation in : 8viui:? 8vj uj :? { and in 0 the corresponding solving relation does not hold: 8vi:u0i:? 6v 8vj :u0j :?, where 8vi:u0i:? 2 0(8vi:Xi) and 8vj :u0j :? 2 0(8vj :Xj ).
There are two cases depending on u0i = or u0i 6= (i) Notice that if u0i = , Xi is an anchor variable, the assumptions and invariants tell us that vj u0j is a proper pre x of vi. vi = vj u0j ri. In this case, we replace 8vj :u0j :? with 8vj :u0j ri:? 2 0(8vj :Xj ). Notice that the solving relation is thus recovered and Xi is still an anchor variable (invariant 2). Notice also that since is a uni er, the invariant 1 is also satis ed. (The pre x for the ?-particle is enforced by the goal subsumption and the ? in 0(Xi).) (ii) If Xi is not an anchor variable in 0 (due to the corrections already done on the ?-particles in 0(Xi)), then by the invariant 2 there is an anchor variable Y , 0(Y ) = ?, such that 0(8v:Y ) + 8vi:u0i:? 2 0(Xi). We do similar correction on the ?-particle 8vj :u0j :? in 0(8vj :u0j :Xj ) as in the previous case. Since 8vi:u0i:? 6v 8vj :u0j :?, vj u0j has to be a proper pre x of viu0i. Hence viu0i = vj u0j ri. We replace 8vj :u0j :? in 0(8vj :Xj ) by 8vj :u0j ri:?.
Notice that here too the invariant 1 is satis ed, since the modi cation preformed is the minimal requirement in order for the solving relation to hold. Hence the string roles have to agree with the string roles in .
After preforming all the transformations, we reduce the concepts in the substitution for the variables and remove the redundant particles.
A simple example of this construction is in Appendix B, Example 6.
From Lemma 2, we know that if there is a cycle in a solution for a uni cation problem, there are anchor variables in the uni cation problem. We can guess them to be ?-variables and solve the subsumptions in which they occur. The solved subsumptions are removed from the unsolved part of the problem, hence the cycles are broken. What is left, are at most some non-cyclic paths, with which we will deal with in the next subsection. 3.4
Now we formulate a kind of reduction lemma, which relates uni cation in F L?
to that in F L0. It is similar to Lemma 9 in [
Lemma 3. Let be an F L? uni cation problem such that ? does not appear as a symbol in . If is a F L? solution of and there are no cycles among ?-particles in ( ), then there is also an F L0 solution for .
Proof. Let be an F L? solution of . By Lemma 1 we can assume that does not have any redundant particles. Since we assume that there are no cycles between ?-particles, we know that ?-particles may only be on paths starting with ?-particles solving some ground A-particles from .
The proof shows how we can eliminate the ? symbols from the solution .
First we construct a substitution B from , such that B is with ? replaced by a new constant B. Hence B = [? ! B].
Obviously, B is an F L0 substitution, but it is not in general a uni er of . We show how to extend B so that it uni es .
Let P be a particle in the range of and P B be the particle P after the replacement in B.
Hence: P B = (8v:A)B = (8v:A if A is not ?
8v:B if A is ?
Each particle P that occurs in the range of is now changed to P B in the range of B. Notice that in the de nition above, v may be empty.
For any goal subsumption C v? D: if (C) v (D), but B(C) 6v B(D), there is a particle P such that B(C) 6v P B, P B 2 B(D).
In this case there is a ?-particle 8v:? 2 (C), such that 8v:? v P B, but now 8v:? is replaced by 8v:B in B(C).
8v:? 2 (8v0:X), where 8v0:X 2 C. This is so, because ? cannot occur as such in C by assumption. v0 may be empty, but it must be a pre x of v, v = v0v00. P B has to have the form 8vvi:A, where vi may be empty and A is either B or any other constant.
In order to regain a uni er, we extend B(X) as follows: B(X) B(X) [ f8v00vi:Ag.
After this extension B(8v0:X) has two particles (among other possible particles): f8v0v00:B; 8v0v00vi:Ag = f8v:B; 8vvi:Ag which replaced 8v:B.5 Hence after the extension B(C) v P B. In such way we repair each dis-subsumption among the goal subsumptions and the extended B becomes a uni er.
Obviously, this extension of B that corrects dis-subsumptions locally, has to terminate in polynomial time, because since there is no cycle in ( ), extending
B, we will nally get to the ?-particles in the range of that are not solved by any other particle (dead-ends for solving relation). If such ?-particle is changed to B-particle in the range of B it will not trigger any more extensions and the additional particles added to the range because of such a B-particle will not need to be solved by any other particle.
The only situation that a new particle might be augmented ad in nitum is when the ?-particles are in a cyclic solving relation. Example 7 illustrates the 5 If we were to replace B back with ?, the second particle would be reduced immediately in the presence of 8v:?. symbols used in the above proof. Example 8 illustrates how the construction breaks when there is a cycle in ( ). 4
The uni cation procedure is as follows: 1. We run ?-elimination ( attening) on . This is explained in the next subsection (subsection 4.1). This step can fail or result with a partial solution ? that maps some variables to ? and a small uni cation problem 0.
If the attening step does not fail, then is F L?-uni able i 0 is.6
2. In subsection 4.2 we consider the uni cation problem 0. 0 does not contain
? symbol, but it may contain ?-variables. We can see that 0 is of such
form that cycles are impossible in any solution of 0. Hence by Lemma 3,
in order to decide if there is an F L? uni er of 0, it is enough to decide
the existence of an F L0-uni er. Hence we run an F L0-uni cation procedure,
which enforces the so called decreasing rule for decomposition variables. We
have to ensure that the F L0-uni er will not increase the number of variables
substituted with ?. For this task we may use the algorithm described in [
This procedure fails or terminates with success in at most exponential time in the size of 0.
P 0 , if P = 8r:P 0 In this section we allow ? symbol in a uni cation problem.
The most important part of the uni cation procedure is a attening step, where we eliminate bottom from the goal subsumptions and atten them.7 Elimination of ? requires guessing which variables are ?-variables. This information is kept as a partial solution. Such guessing causes some goal subsumptions to be removed as solved. We can also fail, if a subsumption is unsolvable due to such guess. First we set the following notation.
If P is a particle, P 6= ? and r a role name (r 2 R), we de ne P r in the following way:
>8P r if P is a variable and then P r is a decomposition variable P r = <
:>> , if P is a constant or P = 8s:P 00, where s 6= r
P r is the so called a decomposition variable. The meaning of this variable is expressed in the following property: for any solution and any ground particle Q, 8r:Q 2 (P ) if and only if Q 2 (P r).
For each role name r and a variable P , there can be only one
decomposition variable denoted by P r. It will be constrained by the so called increasing
6 With an additional requirement of preserving the so called decreasing rule.
7 The procedure presented here is very similar to the attening in [
For the decreasing rule, we cannot have a suitable subsumption which could be added to a uni cation problem, but our algorithm for solving F L? uni cation should secure that this implication is true for any variable P and concept C.
A goal subsumption C v? D, where D is a particle, is called non- at if D = 8r:D0 or there is a particle of the form 8r:C0 2 C.
If s is a non- at goal subsumption, s = C1u uCn v? D, where C1; : : : ; Cn; D are particles not equal to ?, we de ne s r = C1 r u u Cn r v? D r.
If P is a particle, P 6= ? and A is a constant, then we de ne P A in the following way: P A = (P if P is a constant A or a variable
> in all other cases
If s is a goal subsumption, s = C1 u u Cn v? D, where C1; : : : ; Cn; D are particles not equal to ?, we de ne sA = C1A u u CnA v? DA.8
Implicit rule At each step of the following procedure, we implicitly apply the following rule that removes trivially solved equations or fails: { if there is a goal subsumption C v? P such that ? 2 C or P 2 C or P >, then remove this subsumption from the current uni cation problem. { if there is a goal subsumption C v? P such that 8v:> 2 C, then delete the particle from C,
? { fail at once if C v ? is in the goal and ? 62 C.
Step 1. In the rst step we guess which variables in the goal contain bottom and we replace them with ?. We keep the partial solution for the eliminated variables as a set of assignments ([X 7! ?]).
Step 2. We look at the non- at subsumptions.
For a non- at goal subsumption: s = C1 u u Cn v? D we do the following. 1. If D = 8r:D0, then replace s with s r.
If D0 = ?, s r has ? on its right hand side, hence the implicit rule applies. If a new decomposition variable Xr is created in the process of constructing s r, we add the increasing subsumption of the form X v? 8r:Xr. If the decomposition variable Xr is already created, we use it in s r as needed. The increasing subsumption is part of the uni cation problem, but no increasing subsumption is subject to the attening procedure.
We guess if Xr is ? or not. If it is ? then Xr is replaced by ? in all subsumptions except the increasing one. (The implicit rule applies.) 2. If D is a constant, then we replace s with sD. 8 The particles that are not constant A or variables are deleted from s.
Lemma 4. The process of ?-elimination terminates in nondeterministic polynomial time.
Proof. Step 1 terminates because there are only nitely many variables in a given uni cation problem. Step 2 terminates, since there are only polynomially many occurrences of particles of the form 8r:C in a given uni cation problem and each transformation in the step removes at least one of them.
The following theorem states completeness and soundness of ?-elimination w.r.t. uni cation in F L?.
Theorem 1. Let be an F L? uni cation problem and 0 the problem transformed by the ?-elimination steps. A substitution is a solution of i there is a substitution 0 that solves 0 and obeys the decreasing rule. Proof. The "only if" direction (completeness): if is a uni er of , then 0 is a uni er of 0, where 0 is the extension of :
0(Xr) = fP j 8r:P 2 0(X)g.
Notice that 0 obeys the decreasing rule.
It is enough to show the implication for one step of the procedure of ?elimination. 1. For Step 1 and the implicit rule, we just state that the removed subsumptions are trivially satis ed by as well as by 0 augmented with saved partial solution. 2. For Step 2, we assume that a non- at goal subsumption s was selected for the transformation. 0 solves s.
We have several cases to consider. (a) D = 8r:D0. Since 0 solves s, 0(s) has to have either ? on its right hand side or a particle 8r:C0 (C0 v D0). The rst possibility is excluded, since then s would be removed by the implicit rule. Hence there must be 8r:C0 in the particles on its left hand side of 0(s). This particle is either a part of s, or there is 8r:X in s and 8r:C0 2 0(8r:X) or there is a variable Y in s and 8r:C0 2 0(Y ). In the rst case, C0 is on the left hand side of s r, in the second case, C0 2 0(X), in the third case, (by decreasing rule) C0 2 0(Xr). In all these cases 0 solves s r. (b) D is a constant. Since s is solved by 0 and there is no ? at the top level on the left hand side of 0(s), D must be on the left hand side of 0(s).
Hence 0 solves sD as required. (c) D is a variable.
We have two cases here.
{ For a given role name r, there is are particles 8r:P 2 0(D). Then since s is solved by 0 and ? is not at the top level of s, and because of the de nition of 0 for the decomposition variables obeying the decreasing rule, 0 solves also s r. If there is no particle of the form 8r:P in 0(D), then 0(Xr) = >, and s r is also solved by 0. { If there is a constant A in 0(D), then 0 solves D v? A and C1A u u CnA v? A.
For the "if" direction (soundness) we have to show that, if 0 solves 0 and obeys the decreasing rule, then solves . Notice that is the restriction of 0 and the saved partial solution assignments, to the variables in . We have to follow the steps of attening in the opposite direction. Assume that s 2 and s = C1 u u Cn v? D. 1. If s was removed in Step 1 or by the implicit rule, it is solved by any substitution extended with the saved partial solution, hence it is solved by 0 plus saved partial solution assignments. The cases below assume that s was not removed by the implicit rule. 2. If D = 8r:D0, we know that s r replaced s and 0 solves s r. Since 0 satis es the increasing subsumptions, then 0 solves s too. D = 8r:? is a special case, when s r had to be removed by the implicit rule. 3. If D is a constant, s was replaced by sD and 0 solves sD. Since s di ers from sD by having more particles on the left hand side, 0 solves s. 4. If D is a variable, we consider all particles P in 0(D).
{ If P = 8r:P 0, there is a subsumption s r in the goal, 0 solves s r. Thus since 0 solves the increasing subsumptions and obeys the decreasing rule, it solves also subsumption C1 u u Cn v? P . { If P is a constant, then there is a subsumption sA in the goal and 0 solves this subsumption. Hence 0 solves also subsumption C1 u u Cn v? P . Hence since for each particle in 0(D), the corresponding subsumptions are solved by 0, then 0 solves s too. In the case there are no particles in 0(D), 0(D) = > and 0 solves s.
In the next theorem we justify the possbility of using F L0-uni cation on obtained from ?-elimination. 0 Theorem 2. Let be a F L?-uni er of , then there is 0 a uni cation problem obtained from by ?-elimination, such that 0, an extension of , is a uni er of 0 and 0( 0) has no cycles.
Proof. Let 0 be obtained from by ?-elimination, 0 is a solution for 0, where 0 is an extension of to new variables. By Lemma 1 and Lemma 2, we assume that 0 has no redundant particles, and every ?-particle in the cycle is connected with a path to an anchor ?-variable. Since 0 was obtained by ?-elimination, 0( ) has no ?-variables except some decomposition variables occurring in the increasing subsumptions. Hence if there is a cycle in 0( 0), these are the anchor variables for the cycles.
For a ?-variable Xr to be an anchor for a cycle, 0 must contain a subsumption C u 8u1:Xr v? 8u2:Y , where u1; u2 may be empty. It is impossible that u1 is not empty, because 0 contains only at subsumptions.
This cannot be an increasing subsumption, because Xr is ?-variable and thus the subsumption is impossible in 0, because Xr is ?. Hence there cannot be any cycle in 0( 0). Example 9 shows how a cycle is solved by ?-elimination. Theorem 3. (main result) For an F L? uni cation problem at most ExpTime. is decidable in Proof. By Lemma 4, ?-elimination is a procedure non-deterministic polynomial in the size of . If successful, it returns ? a partial solution for the variables eliminated from the goal. The exponential time needed for the F L0-uni cation dominates the non-deterministic polynomial time of the rst step.
Soundness: if both stages of the procedure terminate successfully, then the partial solution ? combined with FL0 [B 7! ?] is a solution for . This is because of soundness of ?-elimination, Theorem 2 and soundness of F L0uni cation procedure. The F L0-uni er should not increase the number of ?variables (variables with B in the substitution).9
Completeness: if there is a solution of , by completeness of ?-elimination, Theorem 1, there is a way to perform ?-elimination in such a way that it will not fail, and we will get a uni cation problem 0. 0 has a uni er with no cycles and obeys the decreasing rule, hence by Lemma 3, there is a F L0-uni er of 0 that obeys the decreasing rule. Hence by completeness of F L0-uni cation procedure we will get the positive answer. 5
The constructions presented in this paper show that the uni cation in F L? can
be solved in ExpTime. The question remains if the problem is also ExpTime hard.
In the solving procedure we are passing the attened problem to a uni cation
procedure for F L0 with a at TBox. This is possible, because we can see our
attened problem as a F L0 uni cation problem with the empty TBox. The next
question arises, if it is possible to extend the algorithm to the case of F L? with
a at TBox. One can try to extend the method of solving uni cation presented
in this paper to other extensions of F L0 and other description logics.
9 In the F L0-uni cation procedure in [
P r = We will be using the following notation. If P is a particle, P 6= ? and r a role name (r 2 R), we de ne P r in the following way: (P 0; if P = 8r:P 0
>; if P is a constant or P = 8s:P 00, where s 6= r
Now if C is a set of the particles fP1; : : : ; Png such that ? 62 C, then C r = fP1 r; : : : ; Pn rg. For the F L? concepts C; D in normal form, C v D holds if for every particle P in D, C v P . Hence in the following steps we decide only C v P for P 2 D.
Step 1. If ? 2 C then return true.
Step 2. If P is ?, then return false.
Step 3. If P is a constant, then return P 2 C.
Step 4. If P = 8r:P 0, then return C r v P 0
Obviously the procedure either terminates at once (Step 1 or Step 2), or terminates after a polynomial inclusion test (Step 3), or calls itself on a strictly smaller problem (Step 4). Hence it has to terminate in the polynomial time. B
The following example illustrates the construction from the proof of Lemma 1. Example 4. Let = f8rr:? u X v? 8r:Xg and = [X 7! fA; 8r:Ag]. is a uni er. The solving relation is as indicated by the arrows over the subsumption.
8rr:? u A u 8r:A v 8r:A u 8rr:A from
Now, there is no particle P , which is solved by A. Hence we can remove it (X). We obtain another uni er, 0 = [X 7! f8r:Ag].
8rr:? u 8r:A v 8rr:A
Now, we discover that no particle is solved by 8r:A in 0(X). By removing it, we obtain another uni er, 00 = [X 7! >] 8rr:? u > 8rr:? v > (1)
The following simple example illustrates the de nition of a cycle (De nition 2).
Example 5. Let the uni cation problem be:
= f8r:U v? X; X v? 8r:Y; Y v? 8s:X; 8s:W v? Y g And let the solution be:
= [U 7! ?; W 7! ?; X 7! 8r:?; Y 7! 8s:?]. 1. An example of a path is: 8r: ? 8r:? ; 8r:? 8r: s:? ; 8s:? 8s: r:?
The arrows indicate which ?-particles are assigned to which variables. 2. The following path obviously intersects with the one above.
8s: ? 8s:? ; 8s:? 8s: r:? ; 8r:?
8r: s:? U;
X;
Y W;
Y;
X 3. A cycle of ?-particles includes all particles in ( ), because all of them are connected by the solving relation. The actual cyclic relation is between the particles involving (X) and (Y ): 8s:?
8s: r:? X;
Y The variables U and W are the so called anchor variables.
The following example illustrates the construction in the proof of Lemma 2. Example 6. Let = fs1 = 8r:U v? Z; s2 = 8rs:Z u 8r:Y v? 8rsr:X; s3 = ? ? X v 8r:A; s4 = X v 8s:Bg
Let = [U 7! ?; X 7! f8r:?; 8s:?g; Y 7! 8srs:?; Z 7! 8rr:?] Step 1. 0 = [U 7! ?; X 7! f?; ?g; Y 7! ?; Z 7! ?] Step 2. s1 = 8r:? 6v ?. Hence the particle ? in 0(Z) is changed to 8r:?. In s2 solving relation is satis ed: 8rs:r:? v 8rsr:?.
Another solving relation in s2 is also satis ed: 8r:? v 8rsr:?.
s3 and s4 are also satis ed. In fact their role is to make all the ? particles non-redundant.
The following example illustrates concepts in the proof of Lemma 3.
Another example illustrates how the above construction is not possible when the ?-particles form a cycle.
The next example illustrates how a cycle is solved by ?-elimination process. (Theorem 1) Example 9. Let X v? 8r:Y; Y v? 8s:X belong to a uni cation problem . If is the solution, the subsumptions must be solved by some cyclic particles in ( ).
If there is a cycle in ( ), we have to guess at least one variable to be ?. Let [X 7! ?] and Y is not a ?-variable. Then the rst subsumption is solved and removed. The second subsumption has the form: Y v? 8s:?. It will be attened to: Y s v? ? and Y v? 8s:Y s (the increasing subsumption). We are forced to guess [Y s 7! ?] (or fail), which yields the solution [X 7! ?; Y 7! 8s:?].