The small description logic F L0 deals with concepts constructed from concept names and roles with conjunction and value restriction for the roles. It is known that deciding the subsumption between concepts in this logic is polynomial, and uni cation is ExpTimecomplete. If we consider the subsumption problem modulo a set of ground axioms the problem is ExpTime-complete. In this paper we study unication in F L0 modulo a set of ground axioms. We do not solve the problem in general, but focus on a very restricted case, namely the case where axioms are at subsumptions between concept names. In this restricted case the subsumption is still polynomial, and we show that the uni cation is ExpTime-complete.
Introduction
On the other hand the presented result can be viewed as a generalization
of our uni cation algorithm from [
In this paper we will analyze the uni cation problem directly, without an
encoding into anti-Horn clauses. The idea though is the same as in [
We assume some knowledge of Description Logics and of F L0 in particular,
and refer the reader to [
Normal form, TBox and subsumption
An F L0 concept C is in normal form2 if it is of the form: 8v1:A1 u u 8vn:An, where vi are words over a set of role names R and Ai 2 N are concept names. If vi = , then 8vi:Ai = 8 :Ai = Ai. Notice that the concept names can be repeated, as they can be reachable by di erent role words. A simple conjunct of a concept in this form, 8vi:Ai, with vi 2 R , is called a particle.
Since an F L0 concept in the normal form is a conjunction of particles, we treat it as a set of particles and use the notation: P 2 C to indicate that P is a conjunct of a conjunction of particles C. Similarly, we use the subset relation to compare conjunctions. In accordance of the meaning of conjunction, the empty conjunction (or the empty set) of particles is understood as >, the concept that subsumes every other concept.
Since in the usual F L0 concept, conjunction can appear also under universal value restriction, changing C into this normal form may increase the size, but only polynomially, since each particle in the normal form of C has to correspond to a unique leaf in the parse tree of the original concept.
Below we assume that all concepts are in this normal form. As sets of particles, we always understand them modulo associativity, commutatity and idempotence, even when we write them using conjunction constructor.
We assume that an F L0 TBox is a set of general concept inclusions (GCIs) between concepts in normal form. These GCIs are also called axioms.
the one that is most suitable for our purposes.
By properties of conjunction and equivalence, we can transform these axioms into the subsumptions with one particle on the right hand-side: 8v1:A1 u u 8vn:An v 8w:B, where vi; w are words over the set of role names R and Ai; B 2 N are concept names.
Equivalence between particles 8v:A 8w:B is just a short form of two subsumptions in the opposite directions.
We de ne a rewrite step as a notion describing an application of an axiom from a TBox T .
C u 8v:C1 u u 8v:Cm vT C u 8v:D is called a rewrite step at position p i C1 u u Cm v D is a GCI in T and v is a word over R of the length p. C in the above de nition is any F L0 concept in normal form and C1; : : : ; Cm; D are particles.
In the presence of a TBox, subsumption between two F L0 concepts C1 vT C2 in normal forms occurs if and only if one of the following cases holds: { C2 C1 (inclusion step) { There is a rewrite step between C1 and C2 at some position. { There is a sequence of inclusion or rewrite steps:
C10 vT C20; C20 vT C30; : : : ; Cn0 1 vT Cn0, such that C1 = C10 and C2 = Cn0. (transitivity of subsumption)
This characterization of subsumption in F L0 follows directly from the semantic properties of constructors of F L0.3
Now, we assume that a TBox has a special form. It contains only at subsumptions of the form: A1 u u An v B, where A1; : : : ; An; B are concept names. We call such TBox a at TBox.
Obviously, in such a TBox, every rewrite step can only have the form C0 u 8v:A1 u u 8v:An vT C0 u 8v:B, where each particle has the same role pre x v.
Hence if this rewrite step is applied to C, C vT D, then there must be particles of the same height: 8v:A1; : : : ; 8v:An in C, and they are replaced by a particle of the same height, 8v:B in D.
Now we show that the subsumption problem w.r.t. a at TBox is in P.4
We de ne a saturation of an F L0 concept C w.r.t. GCIs in a TBox T . In this
de nition [8v:C] denotes a concept 8v:C brought to the normal form. Hence e.g.
[8v:(A u B)] denotes 8v:A u 8v:B or equivalently a set of particles f8v:A; 8v:Bg.
3 Without a TBox, subsumption in F L0 is characterized by the rst and third
condition. In the presence of a TBox, rewrite steps allow us to show additional
subsumptions between F L0 concepts. Since we assume that concepts are in normal form,
they are treated as sets of particles.
4 We follow here the idea from [
C and Saturation terminates (because T is nite and at) and C Obviously, if T is not at, this process may not terminate.
T C.
Lemma 1. Let C; D be F L0 concepts and T a at F L0 TBox. Then C vT D if and only if D C .
Example 1. Let T = fA u B v C; B u C v Dg.
Let C = f8r:A; 8r:Bg.
Then C = f8r:A; 8r:B; 8r:C; 8r:Dg. Obviously, C vT 8r:D Corollary 1. Subsumption problem in F L0 modulo a at TBox is polynomial. Proof. In order to decide if C vT D, we saturate C. This process terminates in polynomial time, because T is nite and the saturation may be executed only the number of times corresponding to the number of GCIs in T times the number of pre xes present in the particles of C.
Most crucial observation for our uni cation procedure is that for every subsumption of the form 8v1:C1 u u 8vn:Cn vT 8v:D, also the subsumption C1 u u Cn vT D holds, where C1; : : : ; Cn; D are constants. This is true for a at TBox. We can prove the following, even stronger result.
Lemma 2. Let T be a at TBox. Then for every v; v0 2 R , 8v:A1 u u 8v:An vT 8v:B if and only if 8v0:A1 u u 8v0:An vT 8v0:B. Proof. If 8v:A1 u at and then 8v0:A1 u u 8v:An vT 8v:B then A1 u u An vT B because T is
u 8v0:An vT 8v0:B by F L0 properties.5 3
Uni cation problem Uni cation problem is de ned as a set of goal subsumptions between F L0 concepts in normal form: = fC1 v? D1; : : : ; Cn v? Dng:
Each of the goal subsumptions contains concepts in normal form, hence it is of the form: 8v1:A1 u u 8vm:Am v? 8v:B, where vi (or v) may be empty and Ai (or B) is a concept name.
Some of the concept names in the goal are variables. The concept names that are not variables are called constants. The set of goal variables is denoted by Var. F L0 concepts, subsumptions and sets of subsumptions that do not contain variables are called ground. We assume a at, ground TBox T .
A solution for the uni cation problem modulo T is a substitution of ground concepts for the variables, such that the goal subsumptions are true modulo the TBox T . Notice that we are searching for ground substitutions, hence if a 5 Value restrictions behave like homomorphism. variable is assigned an empty conjunction of particles, we understand that it is substituted by the top constructor, >. If a goal subsumption is of the form C1 u u Cn v? D, D is a variable, and a substitution assigns > to D, we say that satis es this subsumptions voidly.
The attening of goal subsumptions is a kind of decomposition, which is a part of uni cation procedure. We atten the goal subsumptions by a transformation using fresh variables and adding new goal subsumptions. A goal subsumption C1 u u Cn v? D, where C1; : : : ; Cn; D are particles, is not at if D is of the form 8r:D0 or there is an i, 1 i n, such that Ci is of the form 8r:Ci0. In order to atten such a subsumption, we will introduce decomposition variables, e.g. for a variable X, a decomposition variable would be denoted Xr. Such a variable will be de ned by an increasing subsumption X v? 8r:Xr and a decreasing rule 1 introduced later. An increasing subsumption is added automatically to the uni cation problem, at the moment of the creation of a decomposition variable. The set of increasing subsumptions is maintained separately from other goal subsumptions, and is not subject to attening. For a given role r and a variable X, Xr is unique, if it exists.
In a attening process we will use the following notation. If P is a particle and r a role name (r 2 R), we de ne P r in the following way:
8>P r if P is a variable and P r is a decomposition variable P r = <
Pi0
if Pi = 8r:Pi0 >:> in all other cases
If s is a goal subsumption, s = C1 u u Cn v? D, where C1; : : : ; Cn; D are particles, we de ne s r = C1 r u u Cn r v? D r.
If P is a particle, then we de ne P cons in the following way: P cons = (P if P is a constant or variable
in all other cases >
If s is a goal subsumption, s = C1 u u Cn v? D, where C1; : : : ; Cn; D are particles, we de ne scons = C1cons u u Cnccons v? Dcons.6
The subsumptions obtained in the process of attening are called: { Start subsumptions: of the form C1 u u Cn v? D and D is a constant. { Flat subsumptions: of the form C1 u u Cn v? D and D is a variable. { Increasing subsumptions: of the form C v? 8r:Cr for a role name r.
Now we de ne our attening procedure in Figure 1.
After the attening is done on in an exhaustive way, we can remove the goal subsumptions with > on the right hand-side, as trivially satis ed by any substitution.
The attening process is non-deterministic because of guessing in 3b. This is a polynomial guess, hence the process adds a non-deterministic polynomial step 6 This means that the particles that are not constants or variables are deleted from s. Given a non at goal subsumption: s = C1 u u Cn v? D, 1. If D is of the form 8r:D0,
then replace s with s r. 2. If D is a constant (s is not at, hence there is Ci of the form 8r:Ci0), then replace s with scons. 3. If D is a variable (s is not at, hence there is Ci of the form 8r:Ci0), delete s from and add the following goal subsumptions: (a) for each r 2 R, add s r, (b) guess a set of constants AD in the constants of T and , (c) for each C 2 AD, add { D v? C and { C1cons u u Cncons v? C to the uni cation procedure. The complexity of the uni cation is dominated by the algorithm explained in the next section.
The at subsumptions of the form C1 u u Cn v? D, where D is a variable, may have constants or variables on the left hand sides. We call such subsumptions with constants on the left hand sides, mixed subsumptions.
Now we de ne pure subsumptions by deleting all constants from mixed subsumptions in the goal. For example, if X u A v? Y is a mixed subsumption in , then X v? Y is the corresponding pure subsumption.
Pure subsumptions are not part of the goal, but they have the following property: if uni es pure subsumptions, then it also uni es the corresponding mixed subsumptions. We will use the pure subsumptions later on in our uni cation procedure.
The meaning of a decomposition variable Zr is that in a solution it should hold exactly those particles P , for which 8r:P is in the substitution for Z. The process of solving the uni cation problem will determine which particles should be in the solution of Z.
An increasing subsumption does not su ce to express this relation between the substitution for Z and that for Zr. In order to properly characterize the meaning of a decomposition variable Zr, we need to add another restriction on a substitution, which cannot be expressed as a goal subsumption, but rather as an implication, which we call a decreasing rule:
Z v 8r:P =)
Zr v P (1) where P is a ground particle. The meaning of this restriction is that whenever a ground particle of the form 8r:P is in the substitution for Z, then P has to be in the substitution for the decomposition variable Zr. The reason is illustrated in the next example.
Example 2. Let our uni cation problem contain the goal subsumptions: Z v? 8r:A; 8r:A v? Z; Z v? X; X v? 8r:B. In this example, we assume that the TBox is empty. The attened goal is then: sintacrretassuinbgsusmubpstuiomnsp:tiZonrsv:?ZAv; ? 8Xr:Zrvr;?XBv;?a8trs:Xubrs:umptions: A v? Zr; Z v? X;
The rst start subsumption forces A into a substitution for Zr and thus by the rst increasing subsumption 8r:A must be in the substitution for Z. Similarly, Xr gets B and X gets 8r:B. By the second at subsumption we know that 8r:B must be also in the substitution for Z. But there is nothing that can force B into Zr, if we do not use the decreasing rule. If we do apply the decreasing rule 1, then B is forced into Zr, but then we discover that the goal is not uni able, because A 6v; B.
Without applying the decreasing rule 1, the following substitution would be wrongly accepted as a solution: Z 7! f8r:A; 8r:Bg; Zr 7! fAg; X 7! f8r:Bg; Xr 7! fBg
The process of attening of the uni cation problem obviously terminates in polynomial time with polynomial increase of the size of the goal. It is bounded by the size of the original problem. We call a at uni cation problem, normalized. Lemma 3. Let be a uni cation problem which contains a goal subumption which is not at. Let T be a at F L0 TBox.
There is a right application of a rule from Figure 1, such that and 0 a uni cation problem obtained from by this application satis es the following claim: is a ground solution of w.r.t. T i there is a substitution 0 that is a solution of 0 modulo T , where 0 is an extension of to some new variables.
Notice that the decreasing rule is not mentioned in the formulation of the above lemma. This is because if a substitution (or 0) is a ground uni er of (or 0), then even if the decreasing rule is not satis ed by the assignments of (or 0), this can be easily repaired by rede ning the assignment for every decomposition variable: (Xr) := fP j 8r:P 2 (X)g. Because of this, knowing that a substitution is a solution for , we can assume about it that the decreasing rule is satis ed by it.
Example 3. We illustrate in this example the attening process.
Let = fA u 8s:X v? 8r:Y; B u 8r:Y v? A; 8s:Y u 8r:X v? Xg { Let s = A u 8s:X v? 8r:Y . The rst case of attening applies and s is replaced by s r. s r = > v? Y . { Let s = B u 8r:Y v? A. The second case of attening applies and s is replaced by sA. sA = B v? A { Let s = 8s:Y u 8r:X v? X. The third case applies. We guess that AX = ;.
Then s is replaced by s s and s r. s s = Y v? Xs. s r = X v? Xr. Since two decomposition variables are introduced, we have to add two increasing goal subsumptions. X v? 8s:Xs and X v? 8r:Xr. Additionally we will require that the decreasing rule 1 restricts the assignment for the decomposition variables.
Finally the attened has the form: start subsumption: B v? A; at subsumptions: > v? Y; Y v? Xs; X v? Xr; increasing subsumptions: X v? 8s:Xs; X v? 8r:Xr
We can notice that the goal has a solution for any TBox T for which B vT A. For example a solution assigns > to all variables in .
From a syntactic point of view a shortcut is just a pair (X ; t) where X is a set of variables and t is a vector of sets of particles of the same height. It represents an assignment of corresponding sets of particles from t to variables from X . X (t) = [X1 7! t1; X2 7! t2; : : : ; Xn 7! tn]. We require that X (t) satis es the at clauses of a given uni cation problem. We will also make sure that for each valid shortcut (X ; t) there is a substitution of which X (t) is a part such that all minimal particles of in the range of are in t, and such that satis es all subsumptions of , including decreasing rule for the particles of greater heights.
The idea behind our uni cation algorithm is that a solution may be divided into assignments of the particles of the same height to variables in the uni cation problem. These particles behave in an independent way as far as the satis ability of at clauses is concerned. The only connections between particles of di erent heights is by the increasing subsumptions and the decreasing rule.
If (X ; t) is a valid shortcut and it satis es the decreasing rule for the particles in t it is called closed. If additionally it satis es all start subsumptions, it is called complete. Obviously, there is a solution for a uni cation problem , if there is a shortcut that is complete.
In the following part, we will show that we do not need to look for shortcuts for all possible assignments of all possible particles to variables, which would be impossible, given in nitely many possible particles. We can restrict ourselves to the shortcuts with assignment of sets of constants only. These shortcuts of the form (X ; c), where c is a vector of sets of constants, are called c-shortcuts.
They are de ned as follows.
De nition 1. Let X Var. The pair of set of variables X and a vector of sets of constants c, (X ; c) is called a c-shortcut (for ) if there is a substitution satisfying the following conditions: S1 assigns the constants only from c and only to the variables from X , according to the assignment X (c) de ned by (X ; c).
S2 All subsumptions in and the decreasing rule are satis ed by , with possible exception of start subsumptions.
The height of is maxfjwj j 8w:A 2 range( ) with A a constant g. The height of the shortcut (X ; c) is the smallest height of a substitution satisfying S1 and S2.
A special c-shortcut is of the form (;; ;), hence the empty assignment. This corresponds to the solution that substitutes all variables in the uni cation problem with >. Notice that this substitution satis es all at subsumptions, increasing subsumptions and the decreasing rule. Hence it is a legitimate shortcut. We say that this c-shortcut has height 0.
Theorem 1. A uni cation problem there is a complete c-shortcut for .
has a solution modulo a at TBox T i
An interesting property of some of the c-shortcuts is the following: if (X ; c) is a c-shortcut for some vector c, then it provides a substitution satisfying the conditions of De nition 1. Now for some of these c-shortcuts we can lift this substitution in such a way, that instead of constants it assigns the same constants pre xed with a common word v from R (the particle is 8v:C). We construct a new substitution 0, which assigns to each variable in X particles of the form 8v:C, whenever assigned a constant C. 0 satis es the same subsumptions as with exception of start subsumptions and the decreasing rule activated by the particles replacing constants.7
Not all c-shortcuts have this property. Some subsumptions maybe satis ed by because of constants present on the left side of at, mixed subsumptions. We cannot substitute for constants. Hence in such case, we cannot lift to 0. The possibility of lifting of a substitution to particles of bigger height occurs only if satis es pure counterparts of all at subsumptions in the goal, where the pure subsumptions with > on the left hand-side are satis ed voidly by .
The idea for solving F L0 uni cation w.r.t. a at TBox is the following: compute all possible c-shortcuts of height 0, check if there is a complete cshortcut among them, and if not then identify the c-shortcuts that can be used to compute c-shortcuts for height 1, compute the c-shortcuts of height at most 1 with the help of the shortcuts of height 0, and so on, until we nd a c-shortcut which is complete.
For constructing new c-shortcuts, we de ne a notion of an f -output of a shortcut (X ; c) as a pair (X +f ; c), where X +f = fXf 2 Var j X 2 X g such that c[i] = fC j [Xi 7! C] 2 X (c)g. This means that in X +f (c) the same constant C which was assigned to X is now assigned to Xf . With the help of f -output, we make sure that the decreasing rule will be always satis ed by the solution we search for.
Example 4. In this example we see how c-shortcuts can be used to construct a solution. Let T = fA u C v Bg.
= fstart subsumptions: X v? C; at subsumptions: Y f uA v? X; ZuX v? Y ; increasing subsumption: Y v? 8f:Y f g
The pure counterparts for the at subsumptions are: Y f v? X; Z u X v? Y .
First we compute all c-shortcuts of height 0. Among others we will discover the c-shortcut S1 = (fY; Zg; < fCg; fCg >). Since this shortcut de nes an assignment that satis es the pure subsumptions, we label it as usable. Since this is not a complete c-shortcut (the start subsumption is not satis ed), then we look for other c-shortcuts.
We check if S2 = (fX; Y f ; Y; Zg; < fCg; fCg; fBg; fAg >) is a c-shortcut. For that we need a c-shortcut with Y included, and f -output in S2. We can use S1, because its f -output, (fY f g; < fCg >) is included in S2. S2 is thus a legitimate c-shortcut. It happens also that S2 is complete. 7 Notice that constants never activate this rule.
From the two shortcuts S2 and S1 we can construct the following solution: = [X 7! fCg; Y f 7! fCg; Y 7! fB; 8f:Cg; Z 7! fA; 8f:Cg]. Notice how the decreasing rule 1 is satis ed by the solution, because the f -output of S1 is included in S2. 4
Algorithm The uni cation procedure consists of two stages. 1. Flattening of a given uni cation problem. 2. Running Algorithm Main 1 on the normalized problem.
Since the attening process contains a non-deterministic component (it is in NP), in the case the main algorithm fails, one has to try di erent choice of constants for variables in the process of attening, in the rst step.
Now we look at the algorithms: Algorithm Main 1 and Algorithm nextShortcuts 2. flat denotes the set of at subsumptions from and pure their pure counterparts.
The soundness of the main algorithm follows from Theorem 1. If there is a complete c-shortcut, then there is a solution to the uni cation problem given by De nition 1. The completeness of this algorithm follows from the fact that given a ground solution for a problem, we can extract from it a c-shortcut (X ; c), by grouping in X all variables assigned a constant by , and de ning vector c as a vector of sets of constants assigned to variables by . This shortcut must be complete (start subsumptions are satis ed by and they are satis ed by constants mentioned in (X ; c)). This shortcut must have a height which is equal or smaller than the height of . Hence if Algorithm 2 is sound and complete, the main algorithm will detect the existence of this shortcut and terminate with success. Somewhat technical proof of the correctness of Algorithm NextShortcuts 2 is included in the appendix. Our main result is stated in the following theorem. Theorem 2. F L0-uni cation problem w.r.t. a at TBox is ExpTime-complete
The argument for termination and complexity is based on the following observation. The number of all possible pairs (X ; c) is exponential in the size of T and . Hence the for-loop starting in line 2 in Algorithm 2 is executed exponentially many times and preforms polynomially many steps that take at most exponential time each. Since there are at most exponentially many c-shortcuts, the for-loop starting at line 3 may run only at most exponentially many times until the sets of subsequent shortcuts are the same.
The algorithm presented above is sound and complete for uni cation in F L0 modulo a at TBox. It is also sound and complete for uni cation in F L0 modulo the empty TBox. This is because the subsumption checks in Algorithm 1 and Algorithm 2 are done modulo a given TBox. If a TBox is empty, then the subsumption checks will be just simpler.
In the case of the second algorithm, computing next shortcuts, the check is applied in line 4 (T j= temp( flat)). We do this checks by applying substitution to the subsumptions and checking if they are true modulo the TBox. This check is polynomial, as shown in Section 2. The next check in line 13 (T j= temp( pure)) is done the same way. With the empty TBox, the checks are also polynomial of course.
In the main algorithm, we check if any shortcut in the set of shortcuts is complete (line 5). To do this, we apply the assignment of variables to the start subsumptions and check if they are true modulo the TBox. The start subsumptions can be satis ed only by constants, hence we need to check only the assignment de ned be a c-shortcut, disregarding bigger particles. Hence we do this check by substituting variables given by the shortcut with constants and checking if the start subsumptions are true modulo the TBox. If the TBox is empty, this check is a bit simpler: we check inclusion, without computing the saturation of the left hand sides of the subsumptions.
Of course, with the empty TBox, we could much simplify our procedures.
First the attening of the uni cation problems may be more radical. Constants
can be treated independently from each other. Hence we could split subsumptions
further on, or delete the constants that are irrelevant for a uni er. Moreover the
notion of shortcuts may be simpli ed too, because now vectors of constants
may be required to contain only one constant. (Constants behave independently
from each other). Finally, usable shortcuts will be usable for particles with any
constant, hence we do not even need to mention a constant in their de nition.
These ideas were used in our paper [
Conclusions We have proved the F L0-uni cation problem modulo a at TBox is solvable in ExpTime. The algorithm shown in this paper is based on the notion of shortcuts, i.e. substitutions which satisfy some part of the problem.
This method works for a at TBox. It seems though that it can be applied to other forms of TBoxes, provided that they satisfy some form of the property expressed in Lemma 2. Can we de ne properties of a TBox which has a kind of at normal form, but is not completely at, such that the same algorithm would work for it too?
The result in this paper is of course a small step in the direction of hopefully solving uni cation in F L0 modulo general TBox. Hence one would like to explore how to extend the algorithm for less restricted TBoxes.
Another interesting line of research would also be to study matching in F L0
modulo at TBoxes. In [
Proofs omitted in the paper Lemma 1 (Lemma 1 in the paper). Let C; D be F L0 concepts and T a at F L0 TBox. Then C vT D if and only if D C .
Proof. For the only if direction, let us assume that C vT D. Let C be the saturation of C. Then since C T C, C vT D. If D 6 C , then there is a rewrite step C vT D0 with D0 6 C . But this is impossible since C is a saturation.
For the if direction, just notice that if D C , then by inclusion step, C vT D and since C T C , we have C vT D.
Lemma 2 (Lemma 3 in the paper). Let be a uni cation problem which contains a goal subumption which is not at. Let T be a at F L0 TBox.
There is a right application of a rule from Figure 1, such that and 0 a uni cation problem obtained from by this application satis es the following claim: is a ground solution of w.r.t. T i there is a substitution 0 that is a solution of 0 w.r.t. T , where 0 is an extension of to some new variables. Proof. In the only if direction we assume that is a uni er before a attening step. We de ne extension of for some decomposition variables that are possibly introduced in this step as follows:
0(Xr) := fP j 8r:P 2 (X)g.
This yields immediately that all increasing subsumptions created in the course of attening are satis ed by 0. Also the applications of the decreasing rule 1 are correct. (If 0(X) vT 8r:P , then 0(Xr) vT P .)
We assume also that in the process of attening (Figure 1) if case 3 is to be applied, the set of constants AD guessed in 3(b) is as follows:
AD = fC j C is a constant of T or and C 2 (D)g.
Now we consider the attening steps. 1. Let the attening step be taken as de ned in point 1 of Figure 1. Then s = C1 u u Cn v? D 2 , where D = 8r:D0. The attening step modi es the subsumption in to (C1) r u u (Cn) r v? D0 in 0.
We have to show that if uni es the rst subsumption, 0 uni es the second. If uni es C1 u u Cn v? 8r:D0 it means that (8r:D0) (C1; : : : ; Cn) . This means that also 0(D) 0((C1) r; : : : ; (Cn) r) and thus (C1) r u u (Cn) r v? D0 is uni ed by 0. 2. Let the attening step be taken as de ned in point 2 of Figure 1.
Then s = C1 u u Cn v? D 2 , where Ci = 8r:Ci0 and D is a constant. Since uni es the subsumption, (D) = D (C1; : : : ; Cn) . By the properties of F L0 subsumption w.r.t. a at TBox, we can remove (Ci) from (C1; : : : ; Cn) and still D (fC1; : : : ; Cng n fCig) . Hence 0 uni es the same subsumption with Ci deleted. 3. Let the attening step be taken as de ned in point 3 of Figure 1.
Then C1 u u Cn v? D 2 , where Ci = 8r:Ci0 and D is a variable. We have to show that if uni es the subsumption w.r.t. T , then 0 uni es the subsumptions constructed according to the attening procedure for this case.
{ For all particles of the form 8r:P 2 (D), we can see that s r is satis ed by 0, because the substitution for Dr on the right side of sr is such that 0(Dr) = fP j 8r:P 2 (D)g.
If there is no particle of the form 8r:P , for a particular role r, then sr is satis ed, because then 0(Dr) = >. { For all the constants C 2 (D), we have guessed C 2 AD, and thus Since
C 2 0(D), 0 uni es D v? C and also C1cons u u Cncons v? C.
For the if direction, we trace the attening step backwards. If 0 is a solution for 0, then 0 is also a uni er of . We assume that all the increasing subsumptions are satis ed by 0 and also the decreasing rule 1, read as implication is true under 0.
We look at what kind of attening step was made. 1. In the rst case we get sr from s according to the rst point of Figure 1.
Since 0 uni es sr and the increasing subsumptions are satis ed by 0 then 0 uni es also s. 2. In the second case, we get scons from s, where scons di ers from s only in this that some non- at particles are deleted from its left side. Since these particles cannot play any role in the subsumption of a constant, they are redundant.
Hence if 0 solves scons, it also solves s. 3. In the third case, we have a set of subsumptions that replaced s in 0. The subcases of this case illustrate how di erent particles in 0(D) are solved. We consider them separately.
{ If a particle of the form 8r:P is in 0(D), then we know that P 2 0(Dr) and since 0 solves s r, then s is also solved by the same substitution if D on the right side of s is replaced by 8r:P . { If a constant C of T [ 0 is in 0(D) (case (b)), 0 satis es D v? C and
C1cons u u Cncons v? C, then 0 uni es also C1 u u Cn v? C. These are all possible particles in 0(D), hence 0 uni es s.
Now since all variables added in the attening are not in the original goal and 0 is ground, we can restrict 0 to which is equal to 0 restricted to the goal variables. Then = 0jVar and is a uni er of the original uni cation problem before attening.
Theorem 1 (Theorem 1 in the paper). A uni cation problem lution modulo a at TBox T i there is a complete c-shortcut for . has a soProof. This theorem follows directly from the de nition of c-shortcuts (De nition 1).
First only if direction. Let be a solution for , then it satis es the start clauses. If there are some constants assigned by to variables, we can extract a c-shortcut (Z; c) such that Z contains all variables such that assigns constants to them and c contains sets of constants assigned to these variables. satis es all subsumptions and the decreasing rule, hence this shortcut is complete as required by the theorem.
If there are no constants assigned by to variables, this means that all start clauses are ground. Hence they are satis ed by T . Then the c-shortcut we are looking for is de ned as (;; ;). Notice that the empty substitution8 satis es all at and increasing subsumptions and also the decreasing rule. Hence the shortcut (;; ;) is complete.
For the opposite direction, assume there is a c-shortcut satisfying the assumptions in theorem. Obviously, this shortcut provides a substitution that satis es the conditions of De nition 1, hence has a solution.
Theorem 2 (Theorem 2 in the paper). F L0-uni cation problem w.r.t. a at TBox is ExpTime-complete Proof. Lemma 5, together with Lemmas 3 and 4 below show that the problem is in ExpTime. Uni cation in F L0 with the empty TBox is already ExpTimehard. Hence F L0-uni cation modulo a at TBox is ExpTime-complete. Lemma 3 (Soundness of Alg. Main). If Algorithm 1 terminates with T rue, then there is a solution for modulo T .
Proof. The algorithm terminates with T rue only if there is a complete c-shortcut in Si for i 0. The lemma follows by Theorem 1.
Lemma 4 (Completeness of Alg.Main). If there is a solution ulo T , then Algorithm 1 terminates with T rue. for modProof. Assume there is a solution of modulo T . Then there is a c-shortcut dened as follows: (X ; c), where X = fP j [P 7! C] 2 g and c[i] = fC j Pi 7! C 2 g for a Pi 2 X .
(X ; c) is a complete c-shortcut, because satis es the start subsumptions in . By Lemma 7 (completeness of nextShortcuts), this shortcut will be computed for some height n (equal or smaller than the height of ). Algorithm Main will detect that it is a complete shortcut in line 5. In order to detect this, it will substitute the start subsumptions with the assignment de ned by the shortcut (X ; c) and check if they are true modulo T . Hence the algorithm will return T rue.
Lemma 5 (Termination of Alg. Main). Algorithm 1 terminates within time exponential in the size of and T .
Proof. Since there are at most exponentially many c-shortcuts (compare the proof for Lemma 8), the for-loop starting at line 3 may run only at most exponentially many times until the sets of subsequent shortcuts provided are the same. And each round of the loop terminates in time exponential (Lemma 8). Hence in the worst case, the algorithm will return false after computing all possible c-shortcuts, therefore it will terminate in at most exponential time.
Lemma 6 (Soundness of Alg. nextShortcuts). Let S be in Sout output by Algorithm 2. Then there is a substitution that satis es conditions of De nition 1, and thus S is a c-shortcut.
Proof. The proof is by induction of the height of the shortcuts in the input Sin given to the algorithm. decreasing rule is satis ed because the f -output for a used shortcut is in (X ; c), For the higher particles of the form 8vf:c, all at subsumptions are satised by f for every f , because f satis es all the at subsumptions, and then by Lemma 2, f satis es them too. The increasing subsumptions and the decreasing rule are also satis ed by f , because the adding of a function symbol in the increasing subsumptions or deleting one in the decomposition variables are always done at the top of a particle involved. Hence all subsumptions in are satis ed by except possibly some start subsumptions.
Lemma 7 (Completeness of Alg. nextShortcuts 2). Let be a substitution that satis es the conditions of De nition 1. Then there is a c-shortcut S of some height n that is returned by Algorithm 2, when t Sin contains all the c-shortcuts of heights smaller than n.
Proof. The proof is by induction on the height n of in the lemma. they are assigned to variables Q, for which Qf is not de ned, hence even if Q 7! 8f:C is in , there is no decomposition variable Qf .9 Hence we look for a usable c-shortcut (Z; c), such that X f Z and the f -output of (Z; c) is in (X ; c). If f -output is as required, the decreasing rule will be satis ed.
Since is a model for all subsumptions in , by Lemma 2, we know that such (Z; c) exists.
We can extract from the substitution f = f[X 7! 8vf:C] 2 g that corresponds to such a shortcut. The particles of minimal height in f are of the form 8f:C, where S is a constant. Hence this substitution satis es pure subsumptions in . Thus the shortcut is usable.
It has smaller height than n +1, hence by induction it is provided in the input Sin.
This is true for each function symbol f 2 R, hence the algorithm will not fail for (X ; c) and it will be included in the output Sout.
Lemma 8 (Termination of Alg. nextShortcuts). Algorithm 2 terminates in time at most exponential in the size of and T .
Proof. The number of all possible pairs (X ; c) is exponential in the size of T and .
There are polynomially many variables in Var and there are polynomially many constants in and T . Hence we have exponentially many choices for each variable. Hence there are exponentially many such assignments.
Hence the output Sout cannot contain more than exponentially many shortcuts. Hence the for-loop starting in line 2 is executed exponentially many times and preforms polynomially many steps that take at most exponential time each.