Nominal schemas have recently been introduced as a new approach for the integration of DL-safe rules into the Description Logic framework. The e cient processing of knowledge bases with nominal schemas remains, however, challenging. We address this by extending the well-known optimisation of absorption as well as the standard tableau calculus to directly handle the (absorbed) nominal schema axioms. We implement the resulting extension of standard tableau calculi in a novel reasoning system and we integrate further optimisations. In our empirical evaluation, we show the e ect of these optimisations and we find that the proposed approach performs well even when compared to other DL reasoners with dedicated rule support.
We address the problem of an e cient handling of so-called nominal schema axioms in
tableau calculi for Description Logics (DLs). Nominal schemas have been introduced
recently [
Nominal schemas extend the nominal constructor that is present in many DLs and which allows for specifying a concept as a singleton set with a named individual as member, e.g., the interpretation of the concept fag consists of the element that represents the named individual a. Nominal schemas introduce a new concept constructor fxg, where x is a variable that can only be bound to a named individual from the ABox of the knowledge base. This restriction ensures decidability and is common for nominal schemas as well as for SWRL rules.
We use the same running example as Krisnadhi and Hitzler [
SubmittedPaper to s, and hasConflictingAssignedPaper to c in the remainder. Obviously, this axiom can neither be directly expressed in a DL knowledge base nor as ordinary DL-safe rule (e.g., if we were to express the complex concepts as role atoms, we would have to introduce a variable for the submitted paper, which then would only bind to known ABox individuals). However, such nominal schema axioms can be eliminated by upfront grounding, i.e., by replacing nominal schema axioms with all possible grounded axioms obtained by replacing nominal schemas with nominals, where the nominal schemas with the same variable are always replaced by the same nominal. Upfront grounding is, however, very ine cient. For example, a nominal schema axiom with 3 variables can be grounded for a knowledge base with 100 ABox individuals in 1003 di erent ways, which is prohibitive even for small examples.
A promising approach for e cient reasoning in OWL DL ontologies extended with
nominal schemas, i.e., SROIQV knowledge bases with V denoting nominal schemas,
is to adapt established tableau algorithms (e.g., [
In this paper, we present a novel approach that works by collecting possible
bindings for the nominal schema variables during the application of tableau rules; then,
these bindings are used to complete the processing of the nominal schema axioms. For
this, we extend the widely used technique of absorption (Section 3) to handle nominal
schemas (Section 4.1), and we adapt or add new rules to the tableau calculus
(Section 4.2). We further sketch optimisations and empirically evaluate the proposed
approach (Section 5), before we conclude (Section 6). Further details and an extended
evaluation are available in a technical report [
For brevity, we do not introduce DLs (see, e.g., [
Roughly speaking, the tableau algorithm constructs for an input knowledge base K a completion graph G = (V; E; L; ,˙ ) by decomposing complex concepts with a set of expansion rules. Each node x 2 V (edge hx; yi 2 E) is labelled with the set of concepts L(x) (set of roles L(hx; yi)) and ,˙ records inequalities between nodes. G is initialised with one node for each ABox individual/nominal in the input knowledge base (w.l.o.g. we assume that the ABox is non-empty). In order to guarantee that each node of the completion graph indeed satisfies all TBox axioms, one can use a tableau rule that checks, for each general concept inclusion (GCI) C v D, whether C is satisfied for a node and only then adds D to the node label. Checking whether a complex left-hand side is satisfied can, however, be non-trivial. In order to guarantee correctness, one treats such axioms where C is complex as > v :C t D. Given that > is satisfied at each node, the disjunction :C t D is then added to the label of each node. In practise, one uses elaborate transformations in a preprocessing step called absorption to avoid axioms of the form > v :C t D.
Roughly speaking, the absorption algorithm extracts those conditions of a disjunction for which it can be ensured that if one of these conditions is not satisfied for a node in a completion graph, then at least one alternative of the disjunction is trivially satisfiable. These conditions are then used for expressing the disjunction in such a way that non-determinism can be avoided as much as possible in the tableau algorithm. For example, one would like to avoid treating 9r:(A1 t A2) v 9s:A as > v 8r:(:A1 u :A2) t 9s:A. Any node that does not have an r-neighbour trivially satisfies 8r:(:A1 u :A2) and, hence, the overall disjunction. Thus, we could only add the disjunction to nodes that have at least one r-successor. We can, however, go even further by first identifying nodes that satisfy A1 or A2 and then make sure that their r -neighbour satisfies 9s:A. Hence, the disjunctive axiom can be rewritten into A1 v T , A2 v T and T v 8r :(9s:A), where T is a fresh atomic concept. Here, A1 and A2 have been absorbed (i.e., moved to the left-hand side of the axiom) and the concept T is used to enforce the semantics of the original axiom. We call 8r:(:A1 u :A2) completely absorbable since it no longer contributes a disjunct. The goal of the absorption preprocessing step is, therefore, the extraction of such easy to verify conditions that allow for expressing a GCI by possibly several axioms that ideally do not require a disjunction.
In order to absorb more complex concepts it is often necessary to join several
conditions, say A1 to An. An e cient way to do this is binary absorption [
Since our handling of nominal schemas is based on absorption methods, we next present an improved variant of a recursive binary absorption algorithm, which we then extend to nominal schemas in the next section. The improvements allow for absorbing parts of the axioms partially without creating additional disjunctions. For example, the TBox axiom 9r:(A u 8r:C) v D is, without absorption, handled as > v 8r:(:A t 9r::C) t D. None of the disjuncts can be absorbed completely, but it is nevertheless possible to delay the processing of the disjunction until there is an r-neighbour with the concept A in its label. In order to capture this, the absorption rewrites the axiom such that the disjunction is propagated from a node with A in its label to all r -neighbours (if there are any), which results in A v 8r :(8r:(:A t 9r::C) t D).
In the following, C(i); D(i) are (possibly complex) concepts, A(i); T(i) are atomic concepts with T(i) used for fresh concepts and S is a set of concepts. We assume that all concepts are in the well-known negation normal form (NNF) or we use nnf(C) to transform a concept C to an equivalent one in NNF. Our algorithm uses the following functions to absorb axioms of a TBox T into a new (global) TBox T 0: Algorithm 1 isCA(C) and isPA(C) Output: Returns whether the concept C is Output: Returns whether the concept C is parcompletely absorbable tially absorbable 1: procedure isCA(C) 1: procedure isPA(C) 2: if C = C1 t C2 then 2: if C = C1 t C2 then 3: return isCA(C1) ^ isCA(C2) . 3: return isPA(C1) _ isPA(C2) . 4: else if C = C1 u C2 then 4: else if C = C1 u C2 then 5: return isCA(C1) ^ isCA(C2) 5: return isPA(C1) ^ isPA(C2) 6: else if C = 8r:C0 then 6: else if C = 8r:C0 then 7: return isCA(C0) . 7: return true . 8: else if C = :fag then 8: else if C = :fag then 9: return true 9: return true
. . .
10: else if C = :A then
11: return true
12: end if
13: return false
14: end procedure
. . .
10: else if C = :A then
11: return true
12: end if
13: return false
14: end procedure
Algorithm 2 collectDisjuncts(C; absorbable)
Output: Returns the absorbable/not absorbable disjuncts of the concept C
1: S fCg
2: while (C1 t C2) 2 S do
3: S (S n (C1 t C2)) [ fC1; C2g
4: end while
5: if absorbable = true then return f C 2 S j isPA(C) g
6: else return f C 2 S j :isCA(C) g
7: end if
isCA(C) (isPA(C)), shown in Algorithm 1, returns whether the concept C is
completely (partially) absorbable. We have tagged the lines 3 and 7 with a comment
symbol to highlight where isPA might allow additional absorption in comparison
to isCA. We have indicated with “: : :” that the absorption can further be extended
to other constructors, e.g., to constructors of more expressive DLs [
For simplicity, we assume here that axioms of the form C D are rewritten into
C v D and D v C. An extension that directly and, hence, more e ciently handles
axioms of the form A C is also possible [
To obtain the absorbed TBox T 0, we call for each axiom C v D 2 T the function absorbJoined for the set of absorbable disjuncts, i.e., collectDisjuncts(nnf(:C t D); true), which returns a fresh atomic concept that is used to imply a disjunction of the non-absorbable disjuncts, i.e., collectDisjuncts(nnf(:C t D); false). The methods absorbJoined (Algorithm 3) and absorbConcept (Algorithm 4) are recursively calling Algorithm 4 absorbConcept(C) Output: Returns the atomic concept for the absorption of C 1: if C = C1 u C2 then 2: A1 absorbJoined(collectDisjuncts(C1; true)) 3: A2 absorbJoined(collectDisjuncts(C2; true)) 4: T fresh atomic concept 5: T 0 T 0 [ fA1 v T; A2 v T g 6: return T 7: else if C = 8r:C0 then 8: Anb absorbJoined(collectDisjuncts(C0; true)) 9: T fresh atomic concept 10: T 0 T 0 [ fAnb v 8r :T g 11: return T 12: else if C = :fag then 13: T fresh atomic concept 14: T 0 T 0 [ ffag v T g 15: return T
. . .
16: else return A
17: end if
. C is of the form :A
each other, whereby absorbJoined is joining several atomic concepts with binary
absorption axioms and absorbConcept creates the absorption for a specific concept. For
instance, a concept of the form 8r:C can be absorbed (lines 7–11 of Algorithm 4) by
creating a propagation from the atomic concept Anb, which is obtained for the
absorption of C, back over the r-edge, to trigger a fresh atomic concept T . Note, if C cannot
be absorbed, then absorbJoined returns > and the axiom > v 8r :T is created, which
corresponds to 9r:> v T and, thus, is similar to the well known role absorption [
The absorbJoined function creates binary absorption axioms (Algorithm 3, lines 610) for the atomic concepts returned by absorbConcept. Thus, absorbJoined is joining several conditions into one fresh atomic concept, which can be used for further absorption or to initiate the addition of the remaining and non-absorbable part of the axiom. One can further reduce the number of produced axioms by reusing absorption axioms for concepts that occur more then once.
One can show that concept satisfiability is indeed preserved for the absorbed TBox:
4
In contrast to DL-safe SWRL rules, the left-hand side of axioms with nominal schemas
can be satisfied on arbitrary nodes in the completion graph (even though variables can
only bind to nodes that represent individuals/nominals). As a consequence, axioms
with nominal schemas can influence arbitrary nodes in the completion graph and, thus,
blocking, which ensures termination, easily becomes unsound when typical approaches
for rule processing, such as Rete [
Absorption of Axioms with Nominal Schemas The absorption of axioms with nominal schema variables works very similar to the absorption of ordinary axioms. We could directly extend the absorption algorithm to handle the new concept construct, however, to avoid some special cases for conjunctions C1 u C2 in an absorbable disjunct, where di erent nominal schema variables are used in C1 and C2, we require that conjunctions in absorbable positions are eliminated. This can be done by duplicating the disjunction that is absorbed and by replacing C1 u C2 once with C1 and once with C2. For example, the axiom fxg t A v 9r:fxg is handled as the disjunction (:fxg u :A) t 9r:fxg in the absorption and to eliminate :fxg u :A we replace the original axiom with fxg v 9r:fxg and A v 9r:fxg.
For our absorption algorithm of Section 3, the following two modifications are necessary in order to handle nominal schemas in the remaining axioms: isCA(C) (isPA(C)) is extended to return that a negated occurrence of a nominal schema :fxg is completely (partially) absorbable. absorbConcept(C) of Algorithm 4 must now also handle a negated occurrence of a nominal schema :fxg by absorbing it to O v #x:Tx for which the fresh atomic concept Tx is returned and O is a special concept that is added to the label of all ABox individuals.
The # binder operator, as known from Hybrid Logics [
L(w) or B(8r:C; v) * B(C; w) then L(w) ! L(w) [ fCg and B(C; w) ! B(C; w) [ B(8r:C; v) v1-rule: if A v C 2 K , A 2 L(v), v not indirectly blocked, and C < L(v) or B(A; v) * B(C; v) then L(v) ! L(v) [ fCg and B(C; v) ! B(C; v) [ B(A; v) v2-rule: if (A1 u A2) v C 2 K , fA1; A2g L(v), v not indirectly blocked, and 1. B(A1; v) [ B(A2; v) = ; and C < L(v), or 2. (B(A1; v) 1 B(A2; v)) , ; and C < L(v) or (B(A1; v) 1 B(A2; v)) * B(C; v) then L(v) ! L(v) [ fCg and B(C; v) ! B(C; v) [ (B(A1; v) 1 B(A2; v)) #-rule: if #x:C 2 L(v), v not indirectly blocked, and C < L(v) or fx 7! vg < B(C; v) then L(v) ! L(v) [ fCg and B(C; v) ! ffx 7! vgg gr-rule: if gr(C) 2 L(v), v not indirectly blocked, there exists a variable mapping 2 compVKars(C)(B(gr(C); v)) with C[ ] < L(v) then L(v) ! L(v) [ fC[ ]g individual a, an axiom of the form fag v O, where O is a fresh atomic concept. Since the binders are, therefore, only added to ABox individuals (due to axioms of the form O v #x:Tx), the decidability is retained, whereas the unrestricted extension of a Description Logic with binders easily leads to undecidability of the standard reasoning problems.
Other concepts can be absorbed as before, however, the final atomic concept A created by the absorption cannot initiate the addition of the remaining, non-absorbed part of the axiom in the same way. If the remaining disjuncts D1; : : : ; Dn still contain nominal schemas, then the disjunction has to be grounded with those bindings of variables that have been propagated to A. In the tableau algorithm this can be done dynamically, e.g., with a new “grounding concept” and a corresponding rule. Therefore, if D1; : : : ; Dn still contain concepts with nominal schemas, then A v gr(D1 t : : : t Dn) has to be added to the TBox, where gr( ) is the new grounding concept. For simplicity, let us assume that gr(C) is always used to add the remaining, non-absorbed part of the axiom, even if C or the axiom does not contain any nominal schemas.
Example 1. Our running example 9r:(fxgu9a:fygu9v:fzg)u9s:(9a:fygu9v:fzg) v 9c:fxg can be almost completely absorbed into the following axioms:
O v #x:Tx O v #y:Ty Ty v 8a :T1 O v #z:Tz Tz v 8v :T2 (T1 u T2) v T3 T3 v 8s :T4 (T3 u Tx) v T5 T5 v 8r :T6 (T4 u T6) v T7 T7 v gr(9c:fxg); where Tx, Ty, Tz, T1; : : : ; T7 are fresh atomic concepts. Only 9c:fxg cannot be absorbed and has to be grounded on demand. To keep the example small, we have reused axioms for the absorption of the same concepts, whereas the algorithm of Section 3 would generate for each occurrence of :fyg and :fzg a separate binder concept. 4.2
Tableau Algorithm Extensions We can now extend a standard tableau decision procedure to support (absorbed) nominal schema axioms. Note, we assume that GCIs are handled by two rules: the v1-rule handles GCIs of the form A v C (i.e., a non-absorbable axiom C v D is handled as > v nnf(:C t D)) and the v2-rule handles binary absorption axioms of the form (A1 u A2) v C. These rules and the 8-rule (for transitivity support also the 8+-rule) have to be adapted. The # binders and gr( ) concepts are handled by new rules. In order to propagate variable bindings, we keep a set of mappings that records bindings for variables, for each concept in a node label.
Definition 1 (Variable Mapping). A variable mapping is a (partial) function from variable names to individual names. The set of elements on which is defined is the domain, written dom( ), of . We use for the empty variable mapping, i.e., dom( ) = ;. We associate a concept C in the label of a node v with a set of variable mappings, denoted by B(C; v).
When clear from the context, we simply write mapping instead of variable mapping.
Table 1 shows the adapted and new tableau rules and we describe the not so straightforward extensions in more detail below. The mappings have to be propagated by the tableau rules for the concepts and axioms that are used in the absorption. For example, if we apply the adapted v1-rule to an axiom of the form A v C, we keep the mappings also for the concept C. Note that it is only necessary to extend those rules, which are related to concepts and axioms that are used in the absorption, because if the mappings are propagated to a gr( ) concept, the remaining, non-absorbed part of the axiom is grounded and thus corresponds to an ordinary concept.
Some major adjustments are necessary for the v2-rule that handles binary absorption axioms of the form (A1 uA2) v C. First of all, we want to keep the default behaviour if there are no variable mappings associated to the concept facts for which the rule is applied, i.e., if B(A1; v) [ B(A2; v) = ;, then we add C to the label of v. In contrast, if B(A1; v) , ; or B(A2; v) , ;, we propagate the join of the mapping sets to the implied concept. In the case B(A1; v) = ; and B(A2; v) , ;, we extend B(A1; v) by the empty mapping so that the join of B(A1; v) and B(A2; v) results in B(A2; v), which is then propagated to C. We proceed analogously for B(A2; v) = ; and B(A1; v) , ;. In principle, the join combines variable mappings that map common variables to the same individual name and to point out that the empty sets of mappings are specially handled, we have extended the join operator 1 with the superscript .
Definition 2 (Variable Mapping Join). Two variable mappings 1 and 2 are compatible if 1(x) = 2(x) for all x 2 dom( 1) \ dom( 2). For compatible mappings 1 and 2, 1 [ 2 is defined as ( 1 [ 2)(x) = 1(x) if x 2 dom( 1), and ( 1 [ 2)(x) = 2(x) otherwise. Given two (possibly empty) sets of variable mappings M1, M2, let M1 = f g (M2 = f g) if M1 = ; (M2 = ;) and M1 = M1 (M2 = M2) otherwise. The join M1 1 M2 is defined as f 1 [ 2 j 1 2 M1; 2 2 M2 and 1 is compatible with 2g n f g.
For a concept gr(C) the gr-rule grounds C based on the variable mappings associated to gr(C). Since these mappings might not cover all nominal schema variables that occur in C, it is necessary to extend the mappings with every combination of named individuals for the remaining variables. This so-called completion ensures that only fully grounded concepts are added, which can then be handled as ordinary concepts in the completion graph. Therefore, it is also not necessary to further propagate mappings to such newly added concepts.
L(a0) L(a1) 8 >> #x:Tx; Txffx7!a1gg; T ffy7!a3gg; T ffz7!a4gg; 9> >>>>:<>> T3ffy7!(8ar3;z7 !:Ta64g)gf;fxT7!5faf1x17 !;y7!a1a;y37 !;z7 !a3a;2z47 !gg a4gg; >>;>>=>>>
L(a3) n #y:Ty; Tyffy7!a3gg; (8a :T1)ffy7!a3gg o
a0 r; c s a1 v a a2 a v a3 a4
L(a2) ( T ffy7!a3gg; T ffz7!a4gg; T ffy7!a3;z7!a4gg; ) 1 2 3
(8s :T4)fffy7!a3;z7!a4ggg L(a4) n #z:Tz; Tzffz7!a4gg; (8v :T2)ffz7!a4gg o Definition 3 (Grounding, Completion). For a concept C, Vars(C) is the set of nominal schema variables that syntactically occur in C. A concept C is grounded if Vars(C) = ;.
each nominal schema fxg that occurs in C and x 2 dom( ) with the nominal f (x)g.
by the empty mapping if M = ;, the completion compYK (M) of M w.r.t. Y and a
knowledge base K containing the individuals Inds(K ) is
compYK (M) := f [ fx1 7! v1; : : : ; xn 7! vng j 2 M ; x1; : : : ; xn 2 (Y n dom( ));
v1; : : : ; vn 2 Inds(K )g:
The unrestricted application of generating rules such as the 9-rule can lead to the
introduction of infinitely many new tableau nodes. To guarantee termination, one uses
a cycle detection technique called (pairwise) blocking [
The completion graph in Figure 1 is obtained in the course of testing the consistency of a knowledge base containing the axioms of Example 1 and the assertions: r(a0; a1), s(a0; a2), a(a1; a3), v(a1; a4), a(a2; a3), v(a2; a4). Note, Figure 1 shows only those concepts and variable mappings (in superscripts) that are relevant for the grounding of new concepts in this example. However, since O and thereby also the binder concepts are added to all ABox individuals, additional variable mappings are automatically created for every ABox individual. The joins of the mapping sets are created in the nodes a1 and a2 for the concepts T3 and T5 and finally in node a0 for the concept T7. Only the variable mapping fx 7! a1; y 7! a3; z 7! a4g is propagated to the grounding concept gr(9c:fxg) 2 L(a0) and, thus, by replacing the nominal schema fxg with the nominal fa1g, we have 9c:fa1g as the only grounded concept. Hence, the individual a0 is found to have a conflicting review assignment with the paper a1.
Roughly speaking, it is possible to prove the correctness of our nominal schema absorption technique by a reduction between a completion graph for a TBox with nominal schemas and a standard completion graph for the upfront grounded TBox. Blocking still guarantees termination since only a limited number of variable mappings are introduced.
then a tableau decision procedure (as described above) extended by the rules in Table 1 is a decision procedure for the satisfiability of T .
We have implemented the techniques in the novel reasoning system Konclude that supports SROIQV by (i) upfront grounding and (ii) tableau extensions with di erent optimisations to handle the absorbed nominal schema axioms.
A detailed evaluation can be found in the technical report [
Table 2 shows the rules and the number of matches for each rule in the consistency
check. However, since reasoning with UOBM1nD is non-deterministic, these numbers
might vary between di erent executions and reasoners. Our system requires 1:03 s for
preprocessing and 1:09 s for the consistency test for the ontology without rules. Table 3
then shows the increases in reasoning time for the ontology with nominal schema
axioms. In parenthesis we show the additional preprocessing time for the upfront
grounding, which is mostly spend on absorption, lexical normalisation, etc. Upfront grounding
fails for R5 since although two variables can be eliminated (see safety condition in [
Table 3 further shows the reasoning time increase for HermiT and Pellet when a rule from Table 2 is added. Without rules Konclude requires 1:09 s, HermiT 23:24 s, and Pellet 2:22 s for a consistency test (ignoring loading and preprocessing time). With backwards chaining and the propagation of representatives, the reasoning times for Konclude are significantly faster than HermiT’s or Pellet’s. HermiT uses, however, significantly less memory than the other systems. This might be because HermiT does not support complex roles, such as hasSameHomeTownWith in R3, in the body of rules and its results might be incomplete. 6
We have addressed the problem of practical reasoning with nominal schemas through an extended absorption algorithm and with slight modifications of standard tableau calculi. Our approach “collects” the bindings for nominal schema axioms that have to be grounded and considered for a specific node in the completion graph. The presented techniques have been implemented and our empirical evaluation, which focusses on DL-safe rules, shows that our approach works well even compared to reasoners with dedicated rule support.
The first author acknowledges the support of the doctoral scholarship under the Postgraduate Scholarships Act of the Land of Baden-Wuerttemberg (LGFG).
Correctness of the Absorption Algorithm In the following we prove the correctness of Theorem 1, i.e., the correctness of our modified absorption algorithm presented in Section 3. We first show that the complete absorption of a disjunct of an axiom is correct, i.e., it preserves the satisfiability (Lemma 1 and Lemma 2), and then we show that the correctness of a partially absorbed concept disjunct can be reduced to the complete absorption (Lemma 3).
Lemma 1 Let T denote a TBox, I = ( I; I) an interpretation such that I j= T , C a concept that is completely absorbable, A the concept returned by absorbJoined(fCg), and T 0 the extension of T with all the axioms created by absorbJoined(fCg), then 1. for every extension I0 of I such that I0 j= T 0, it holds that I0 j= T , 2. for every extension I0 of I such that I0 j= T 0, it holds for all 2 I0 that 2 AI0 if < CI0 , and 3. there exists an interpretation I0 = ( I0 ; I0 ) such that I0 j= T 0 with I0 = I and 2 AI0 only if < CI0 .
Proof. (Claim 1) Since T 0 is an extension of T , it trivially follows that I0 j= T . (Claim 2) We first prove the simple cases where C is completely absorbable and afterwards we show by induction that the lemma also holds for the complex cases.
If C is of the form :A, then absorbConcept(C) directly returns A, which is then also returned by absorbJoined(fCg). Thus, if 2 I0 and < CI0 , i.e., < (:A)I0 , then 2 AI0 . Hence, the lemma holds if C is of the form :A.
If C is of the form :fag, then absorbConcept(C) adds the axiom fag v A to T 0 and returns A, which is then also returned by absorbJoined(fCg). Thus, if < CI0 , i.e., < (:fag)I0 , then 2 aI0 and because, by assumption, I0 j= T 0, i.e., I0 j= fag v A, it follows that 2 AI0 . Hence, the lemma holds if C is of the form :fag. For the complex cases we assume that all nested disjunctions are replaced by a single disjunction with all disjuncts, i.e., (C1 t (C2 t C3)) is replaced by (C1 t C2 t C3). Furthermore, we automatically decompose a disjunction into the set of disjuncts by calling absorbJoined. This simplification is also done by the algorithm with the collectDisjuncts function, which is always called before absorbJoined. Therefore, we can omit collectDisjuncts for calling absorbJoined, which improves the readability. Now, for a disjunct C j, it follows that C j is not a disjunction itself and it also follows that absorbJoined(fC jg) only returns the atomic trigger concept that is returned by absorbConcept(C j).
Let C1; : : : ; Cn be completely absorbable concepts and A1; : : : ; An the atomic concepts returned by absorbJoined(fC1g); : : : ;absorbJoined(fCng). By our induction hypothesis, the lemma holds for A1 w.r.t. C1; : : : ; An w.r.t. Cn.
If C is now of the form C1 t : : : t Cn, then absorbJoined(fC1; : : : ; Cng) collects the atomic concepts A1; : : : ; An by calling absorbConcept(C j) for each C j, 1 6 j 6 n, and creates the binary absorption axioms (A1 uA2) v T1; (T1 uA3) v T2; : : : ; (Tn 2 u An) v A. Thus, if < CI0 , i.e., < (C1 t : : : t Cn)I0 , then 2 (:C1 u : : : u :Cn)I0 and as a consequence 2 (:C j)I0 for 1 6 j 6 n. Therefore, by the induction hypothesis we have 2 A Ij0 for all 1 6 j 6 n. Thus, 2 A1I0 and 2 A2I0 and since the interpretation I0 j= T 0 with f(A1 u A2) v T1; (T1 u A3) v T2; : : : ; (Tn 2 u An) v Ag T 0 it follows that 2 T1I0 ; 2 T2I0 ; : : : ; 2 AI0 . Hence, the lemma holds by induction if C is of the form C1 t : : : t Cn.
If C is of the form C1 u C2, then absorbJoined(fCg) returns A, which is obtained by calling absorbConcept(C), where additionally the axioms A1 v A and A2 v A are created. If < CI0 , i.e., < (C1 u C2)I0 , then 2 (:C1 t :C2)I0 . There are now two cases: If 2 (:C1)I0 , then by the induction hypothesis we have 2 A1I0 and due to the axiom A1 v A we have 2 AI0 . For the other case we have 2 (:C2)I0 and by the induction hypothesis 2 A2I0 and due to the axiom A2 v A we also have 2 AI0 . Hence, the lemma holds by induction if C is of the form C1 u C2. If C is of the form 8r:C1, then absorbConcept(C) creates A1 v 8r :A and A is returned by absorbJoined(fCg). Thus, if < CI0 , i.e., < (8r:C1)I0 , then 2 (9r::C1)I0 . It follows that there exists 2 I0 , ( ; ) 2 rI0 with 2 (:C1)I0 and by the induction hypothesis we have 2 A1I0 . As a consequence of the axiom A1 v 8r :A we also have 2 AI0 . Hence, the lemma holds by induction if C is of the form 8r:C1.
(Claim 3) We construct the interpretation I0 from I such that 2 AI0 only if < CI0 . Therefore, let I0 = ( I0 ; I0 ) be an interpretation with I0 = I and I0 reduced from I such that only the atomic concepts, atomic roles, and individuals occurring in T are interpreted. Obviously, it still holds that I0 j= T since the interpretation of all axioms in T coincides with I. We now define the interpretation of the fresh atomic concepts A1; : : : ; Am introduced for the absorption of C in I0. Note that we treat absorption axioms of the form A0 v 8r:Ai in their equivalent form 9r :A0 v Ai.
Now, for 1 6 i 6 m and for each axiom H v Ai generated by the absorption, we exhaustively add 2 I0 to AiI0 if (i) H = A0 and 2 A0I0 , (ii) H = fag and 2 fagI0 , (iii) H = (A0 u A00) and 2 A0I0 \ A00I0 , or (iv) H = 9r :A0 and 2 (9r :A0)I0 , i.e., has some r-neighbour such that ( ; ) 2 rI0 and 2 A0I0 . We have 2 AiI0 only if satisfies the left-hand side of an axiom A0 v Ai, fag v Ai, or (A<0 uAIA0 00i)f v Ai, or 9r :A0 v Ai. Consequently, it follows that I0 j= T 0. Furthermore, 2 CI0 , because of the following cases:
If C is of the form :A and 2 CI0 , i.e., 2 (:A)I0 , then < AI0 .
If C is of the form :fag for which the absorption has generated fag v A and if 2 CI0 , i.e., 2 (:fag)I0 , then < fagI0 and then < AI0 , because the left-hand side of fag v A is not satisfied and there is also no other axiom that implies A, because A is freshly used for fag v A.
For the remaining cases, we again assume that the lemma holds for A1 w.r.t. C1; : : : ; An w.r.t. Cn, where A1; : : : ; An are the atomic trigger concepts for absorbing the completely absorbable concepts C1; : : : ; Cn. Therefore, it follows by induction that < AI0 if 2 CI0 , because:
If C is of the form C1t: : :tCn and 2 CI0 , i.e., 2 (C1t: : :tCn)I0 , then there exists a C j, 1 6 j 6 n with 2 C Ij0 . By the induction hypothesis it follows that < A Ij0 satisfied. and by the binary axiom chain (A1 u A2) v T1; (T1 u A3) v T2; : : : ; (T j 2 u A j) v T j 1; : : : ; (Tn 2 u An) v A, which is generated for absorbing C1 t : : : t Cn, we have < AI0 , because the left-hand side of the axiom (T j 2 u A j) v T j 1 cannot be If C is of the form C1 u C2 and 2 CI0 , i.e., 2 (C1 u C2)I0 , then 2 C1I0 and 2 CI0 . By the induction hypothesis we have 2 < AI0 and 1
2 < AI0 . The left-hand generate other axioms that imply A. Thus, is not added to AI0 . side of the axioms A1 v A and A2 v A is not satisfied and the absorptions does not If C is of the form 8r:C1 and with ( ; ) 2 rI0 we also have 2 CI0 , i.e.,
2 (8r:C1)I0 , then for all 2 CI0 . By the induction hypothesis it follows that
1 satisfied, and there are not any other axioms that imply A, we do not add < A1I and since the left-hand side of the generated axiom 9 r :A1 v Ai is not and, thus, < AI0 . 2 to AI0
I0 tu
We can now use Lemma 1 to show the correctness of the absorption for the case of a completely absorbable concept C in an axiom C v D.
and D is neither completely nor partially absorbable, let T1 denote the TBox with T1 = T [ f> v C t Dg and T2 denote the TBox with T2 = T [ f
the axioms created by A respect to T1 i it is satisfiable with respect to T2.
absorbJoined(fCg). Then, a concept C0 is satisfiable with 2
I2 and, therefore, I2 j= T1. (and thus satisfied for every Proof. If direction: For I2 an interpretation with C0I2 , ; and I2 j= T2, we show that I2 j= T1. Because of the axiom A v D 2 T2 for each 2
I2 it holds that either < AI2 2 CI2 by Lemma 1) or
2 DI2 . Thus, the axiom > v (C t D) 2 T1 is that and for all C0I1 , ;, then C0I01 , ;.
Only if direction: For I1 an interpretation with C0I1 , ; and I1 j= T1, we construct an interpretation I01 with C0I01 , ; and I01 j= T2. Since I1 j= T1 and T1 is an extension that can be constructed from I1 for which it holds that I01 j= T [ X and for all 2 AI01 only if < CI01 . Thus, it also follows that I01 j= A v D, because 2 I01 = 2
I01 it holds that either 2 CI01 and thus < AI10 or 2 DI01 . Thus, if
In order to show the correctness of the partial absorption of a disjunction C t D, where C is partially absorbable and D is neither completely nor partially absorbable, we reduce the problem to the complete absorption of C0 t C t D, where for C0 it holds that C0 is completely absorbable and C0 v C. We show that the partial absorption of C is equivalent to the complete absorption of the concept C0. Therefore, the partial obviously equisatisfiable to C t D since C subsumes C0. absorption of C t D corresponds to the complete absorption of C0 t C t D, which is absorbable.
Proof. If C is already completely absorbable, then the lemma trivially holds since in this case C0 is C. Thus, we show in the following for all cases where C is partially absorbable but not completely absorbable that absorbJoined(fCg) generates the absorption of a more specific concept C0 for which it holds C0 v C and C0 is completely absorbable.
If C is of the form 8r:D0 and D0 (nnf(:D0)) is neither completely nor partially absorbable, then absorbConcept(C) creates > v 8 complete absorption of 8r::> for which it holds that 8r::> v 8r:D0. r :A, which corresponds to the To prove the complex cases by induction, we assume that the concepts D1; : : : ; Dm are partially absorbable and the lemma holds for D1; : : : ; Dm, i.e., the absorption completely absorbs the concepts D01; : : : ; D0m, for which it holds that D01 v D1; : : : ; D0m v Dm, and let A1; : : : ; Am be the atomic trigger concepts that are achieved for absorbing D01; : : : ; D0m. creates A1 v 8 If C is of the form 8r:D1 and D1 is partially absorbable, then absorbConcept(C) r :A, where A1 is the atomic trigger concept that is returned by absorbConcept(D1) for completely absorbing D01. The absorption of C corresponds to the complete absorption of 8r:D01 and, by the induction hypothesis, we have D01 v D1. Thus, it also holds that 8r:D01 v 8r:D1.
If C is of the form D1 t : : : t Dm tC1 t : : : tCn with D1; : : : ; Dm partially absorbable and C1; : : : ; Cm neither partially nor completely absorbable, then the absorption creates the binary axiom chain (A1 u A2) v T1; (T1 u A3) v T2; : : : ; (Tm 2 u Am) v A, which corresponds to the complete absorption of D01 t : : : t D0m, where A1; : : : ; Am are again the atomic trigger concepts for absorbing D01; : : : ; D0m. Because of the induction hypothesis it holds that D01 t : : : t D0m v D1 t : : : t Dm t C1 t : : : t Cn. If C is of the form D1 u D2 with D1; D2 partially absorbable, then the absorption creates the axioms A1 v A and A2 v A, which corresponds to the complete absorption of D01 u D02, where A1 and A2 are the atomic trigger concepts for absorbing D0 1 and D02. Because of the induction hypothesis it holds that D01 u D02 v D1 u D2. tu A.2
Correctness of Nominal Schema Absorption In the following we prove the correctness of Theorem 2, i.e., our nominal schema absorption technique presented in Section 4. For this, we roughly proceed as follows: is constructed by a standard tableau algorithm.
Given a nominal schema axiom C v D and an absorbed TBox T , then for Tns and Tug as the TBoxes obtained from absorbing T [ fC v Dg and T [ fU1; : : : ; Uhg, respectively, where U1; : : : ; Uh are the upfront grounded axioms of C v D, we show that a fully expanded and clash free completion graph Gns for Tns can be converted to a fully expanded and clash free completion graph Gug for Tug. Furthermore, we show that our extended tableau algorithm constructs a complete and clash free completion graph Gns for Tns if there exists a fully expanded and clash free completion graph Gug for Tug that
Please note that we only work with TBoxes instead of knowledge bases. This aswith K = (T ; ;). sumption is w.l.o.g. since in the presence of nominals ABoxes can be internalised (e.g., C(a) is equivalent to the GCI fag v A, r(a1; a2) to fag v 9r:fbg, etc.). We assume, therefore, that a completion compYT (M) is analogously defined to the completion compYK (M)
To simplify the conversion between a completion graph for Tns and a standard completion graph for Tug, we ensure that all concept facts can directly be converted into concept facts for the other completion graph. Therefore, we make the following simplifying assumptions: We assume that the absorption of nominals of the form :fag generates fag v > u A instead of fag v A (cf. Algorithm 4, line 14), which is obviously logically equivalent. As a result, binder concepts such as #x:A can be directly converted to concepts of the form > u A. We also assume that the absorption of the upfront grounded axiom C[ ] v D[ ], by the variable mapping , creates a new special grounding concept gr (D) to add the remaining, non-absorbable part of the axiom instead of directly implying D[ ]. This new concept construct retains the mapping and corresponds to the grounding concept gr(D) that is created for the absorption of the nominal schema axiom C v D.
Before introducing the actual conversion, we first define the notion of concept and axiom set closure:
is closed under sub-concepts of C0 and also contains C0. Additionally, fclos(Z) is the extension to a set of axioms Z:
[
C0vD02Z fclos(Z) := clos(:C0 t D0):
aclosT (C0 v D0) := fclos(X10; : : : ; Xn0) n (fclos(T ) [ clos(D0)); where X10; : : : ; Xn0 are the axiom introduced by the absorption of C0 v D0. Note that the concepts in the absorption closure are those that are relevant for the conversion between completion graphs since these are the concepts with variable mappings.
Now, the actual conversion of concepts and axioms obtained from the absorption is defined as follows:
completely and D not completely absorbable, and let be a mapping with dom( ) =
by absorbing T [ fC v Dg and T [ fU1; : : : ; Uhg, respectively, where U1; : : : ; Uh are the axioms obtained by the upfront grounding of C v D. We denote the axioms (in creation order) and fresh atomic concepts obtained by absorbing nnf(:C t D) with X1; : : : ; Xn and A1; : : : ; Ag, respectively. Similarly, we use X1 ; : : : ; Xn and A1; : : : ; Ag for the case of absorbing nnf((:C t D)[ ]).
For the concept C0, we inductively define the concept conversion conv (C0) of C0 w.r.t. T , C v D and as 8>C0 > > > conv (C0) = <>>>>(> u conv (C00)) if C0 = #x:C00 >>>gr (D) if C0 = gr(D) > >>>>:C[0A1=A1;:::;Ag=Ag] otherwise, if C0 < aclosT (C v D) with Ai , for 1 [A1=A1;:::;Ag=Ag]
denotes the syntactic replacement of each occurrence of Ai in C0 i g. The extension to axioms fconv (X) is defined as:
8 fconv (X) = <>>f (x)g v > u conv (D0) if X = O v #x:D0 >>:conv (C0) v conv (D0) otherwise.
In the remainder of the section, we use C v D, , T , Tns, Tug, A1; : : : ; Ag, A1; : : : ; Ag, X1; : : : ; Xn, and X1 ; : : : ; Xn as in the above definition.
Note that the restrictions on C v D are w.l.o.g. since any nominal schema axiom can be transformed into the desired form in an equivalence preserving manner. If nnf(:C) is only partially absorbable, then a completely absorbable concept nnf(:C0) can be extracted from C (cf. Lemma 3), which can be used to obtain an axiom C0 v D0, where it holds that C0 v C, C0 is completely absorbable and D0 = nnf(:C0) t D is not completely absorbable. Also note that :> and ? can always be used to extend a disjunction that corresponds to an axiom in order to obtain a completely absorbable and not completely absorbable disjunct w.r.t. our absorption algorithm.
We can now show that we can convert the axioms obtained by absorbing nnf(:CtD) from the nominal schema axiom C v D into the axioms that are obtained by absorbing the grounded version nnf((:C t D)[ ]), which is the first step in the conversion of a completion graph with nominal schema concepts to a standard completion graph: fX1 ; : : : ; Xn g.
the upfront grounding,
a mapping, Tns and Tug TBoxes, and X1; : : : ; Xn and X1 ; : : : ; Xn axioms as in Definition 5. The set ffconv (X1); : : : ; fconv (Xn)g is identical to the set Proof. Let A1; : : : ; Ag and A1; : : : ; Ag be the fresh atomic concepts introduced by the absorption of nnf(:C t D) and nnf((:C t D)[ ]), respectively. Since the concepts nnf(:C t D) and nnf((:C t D)[ ]) only di er in the nominal schemas that are replaced by nominals, the absorption of nnf(:C t D) and nnf((:C t D)[ ]) is identical expect for axioms of the form O v #x:Ai and Ag v gr(D) in Tns, which correspond to axioms of the form fag v (> u Ai ) and Ag v gr (D) in Tug. Hence, by Definition 5, the claim holds. tu
For the conversion, we use the implicitly associated sets of variable mappings, which are defined as follows: Definition 6 (Implicitly Associated Mappings). The implicitly associated set of variable mappings mappG(C0(v)) for a concept fact C0(v) and C0 in the absorption closure w.r.t. a completion graph G = (V; E; L; B) is defined as: mappG(C0(v)) = <>>>B(C0; v) 8 >>>ffx 7! vgg if C0 = #x:D0 > > >:>f g if B(C0; v) , ; otherwise.
Now, let Gns be a completion graph showing the satisfiability of the TBox Tns. We can replace each concept fact C0(v) with the implicitly associated variable mappings M and C0 2 aclosT (C v D), by the concept facts (conv 1 (C0))(v); : : : ; (conv k (C0))(v), where 1; : : : ; k are the mappings obtained from the completion compVTars(:CtD)(M) of M. As a result, we obtain a fully expanded completion graph Gug that shows the satisfiability of the upfront grounded TBox Tug.
Proof. Let Gns = (Vns; Ens; Lns; ,˙ns; Bns) be a fully expanded and clash free completion graph for Tns. We convert Gns into a fully expanded and clash free completion graph Gug by replacing every concept fact C0(v), C0 2 aclosT (C v D), v 2 Vns, with the implicitly associated variable mappings M = mappGns (C0(v)), by the concept facts (conv 1 (C0))(v); : : : ; (conv k (C0))(v) with f 1; : : : ; kg = compVTars(:CtD)(M). Furthermore, let 2; : : : ; ` be all possible variable mappings for Vars(:C t D) w.r.t. T , i.e., f 2; : : : ; `g = compVTars(:CtD)(f g).
In the following we show that none of the standard tableau rules for the concepts
and axioms used in the absorption are applicable to Gug. Please note that the extended
tableau rules (Table 1) coincide with the standard tableau rules [
We firstly consider the application of the 8-rule, which is not applicable for Gug, because C0 = 8r:D0(v) is converted to (conv 1 (8r:D0))(v); : : : ; (conv k (8r:D0))(v) and for each r-neighbour node w of v the concept fact D0(w) is either also not associated with variable mappings (which is ensured by the absorption algorithm by creating separate axioms with fresh atomic concepts for the absorption of concepts that do not contain nominal schemas) or is at least also associated with the same variable mappings (otherwise the 8-rule would be applicable for Gns) and thus D0(w) is at least also converted to (conv 1 (D0))(w); : : : ; (conv k (D0))(w).
We now consider the application of the v1-rule. The absorption creates axioms of the form H v D0 with D0 2 aclosT (C v D) and H = fag or H = A. If D0 , #x:D00 (the replacement axioms for O v #x:D00 are considered together with the #-concepts), H < aclosT (C v D) and H = A or H = fag, then we would have the axioms H v conv 2 (D0); : : : ; H v conv ` (D0) in Tug and the v1-rule is not applicable, because, for every node v in Gns with the concept fact H(v), D0(v) is also present and Bns(D0; v) = ;. Thus, D0(v) is replaced by (conv 2 (D0))(v); : : : ; (conv ` (D0))(v). If A 2 aclosT (C v D), then we would have the axioms conv 2 (A) v conv 2 (D0); : : : ; conv ` (A) v conv ` (D0) and the v1-rule is not applicable, because for every node v in Gns with the concept fact A(v) and the associated variable mappings 1; : : : ; k, A(v) would be replaced by (conv 1 (A))(v); : : : ; (conv k (A))(v), and D0 is either also not associated with variable mappings (which is ensured by the absorption algorithm) or is at least also associated with the variable mappings 1; : : : ; k (otherwise Gns would not be fully expanded), and is at least also replaced by (conv 1 (D0))(v); : : : ; (conv k (D0))(v). Thus, the v1-rule is not applicable for Gug. Next, we consider the application of the v2-rule for an axiom (A1 u A2) v D0. There are three cases: 1. If Bns(A1; v) = ; and Bns(A2; v) = ;, then Bns(D; v) = ; and every concept fact D0(v) is replaced by (conv 2 (D0))(v); : : : ; (conv ` (D0))(v) and thus the rule is not applicable for (A1 u A2) v conv 2 (D0); : : : ; (A1 u A2) v conv ` (D0). 2. If Bns(A1; v) , ; (Bns(A2; v) , ;), then the v2-rule is analogously to the v1-rule not applicable, because either there is no variable mapping that is associated to A2(v) (A1(v)) and, as a consequence, there is also no variable mapping associated to D0(v) (which is ensured by the absorption algorithm), or every variable mapping that is associated to A2(v) (A1(v)) is also associated to D0(v) if A1 (A2) is also in the label of v. Thus, the v2-rule cannot add a conv j (D0) concept to v that is not already present, because the corresponding conv j (A1) (conv j (A2)) is missing. 3. If Bns(A1; v) , ; and Bns(A2; v) , ;, the v2-rule is again not applicable after the conversion, because A1(v) and A2(v) are replaced by the concept facts (conv 1 (A1))(v); : : : ; (conv k (A1))(v) and (conv 01 (A2))(v); : : : ; (conv 0k0 (A2))(v), respectively, where 1; : : : ; k and 01; : : : ; 0k0 are the completion of the set of variable mappings mappGns (A1(v)) and mappGns (A2(v)). The v2-rule is, however, only applicable for an axiom (conv (A1) u conv (A2)) v conv (D0) if conv (A1) as well as conv (A2) is in the same label, but conv (D0) is not already present, i.e., 2 f 1; : : : ; kg and 2 f 01; : : : ; 0k0 g, but < f 1; : : : ; kg 1 f 01; : : : ; 0k0 g, which is a contradiction, because f 1; : : : ; kg 1 f 01; : : : ; 0k0 g is the same as the completion of Bns(A1; v) 1 Bns(A2; v) to all possible variables used in C v D.
The #-concepts are more complicated. Concept facts of the form #x:D0(a) are not explicitly associated with variable mappings. However, because of the axiom O v #x:D0, they only occur in the label of ABox individual nodes. Thus, we can use the implicit information that x will be bound to the ABox individual node a, and we use the completion of the variable mapping fx 7! ag for 1; : : : ; k. Therefore, we replace #x:D0(a) with the concept facts (>uconv 1 (D0))(a); : : : ; (>uconv k (D0))(a). It is not hard to see that (> u conv 1 (D0)); : : : ; (> u conv k (D0)) cannot be unfolded in Gug, because the #-rule ensures that D0 is also already present in the label of the node and is associated with the variable mapping fx 7! ag and, thus, D0 is also replaced by conv 1 (D0); : : : ; conv k (D0). Analogously, for the axioms fag v > u conv 1 (D0); : : : ; fag v > u conv k (D0) that we have to consider in Gug instead of O v #x:D0, the rules for these axioms are also not applicable, because the concept #x:D0 in the label of a has been replaced by the concepts > u conv 1 (D0); : : : ; > u conv k (D0) and #x:D0 is in the label of a, because it is added to every ABox individual node due to the axiom O v #x:D0.
The argumentation for the gr-concepts and the corresponding rules is very similar.
As mentioned before, we assume that the grounding concept is always used to
add the remaining, non-absorbable part of the axiom. Thus, gr(D) is always in
aclosT (C v D), even if Vars(D) = ;. Furthermore, we also use the assumption
that the absorption of an upfront grounded axiom, by the variable mapping , also
uses a special grounding concept gr (D), which has to be unfolded to D[ ] and
is, therefore, not problematic for the tableau algorithm, because it corresponds to
a conjunction with only one conjunct. Thus, a concept fact gr(D)(v) is replaced
by (conv 1 (gr(D)))(v); : : : ; (conv k (gr(D)))(v), which is the same as (gr 1 (D))(v);
: : : ; (gr k (D))(v). Obviously, these replaced grounding concepts cannot be unfolded
to D[
Next, we show that we can steer our extended tableau algorithm to construct a complete and clash free completion graph Gns for Tns if there exists a fully expanded and clash free completion graph Gug for Tug that is constructed by a standard tableau algothere is a fully expanded and clash free completion graph for Tns.
Proof. Let Gug be a completion graph for Tug that is obtained by applying only rules for concepts and axioms of T . Since our extended rules coincide with the standard tableau rules if no variable mappings are associated to concept facts, our extended tableau algorithm can create Gns, which exactly coincides with Gug. We show that the application of a rule in Table 1 to Gns deterministically adds only concept facts and possibly variable mappings, for which the conversion of these facts and variable mappings are also consequences in Gug that are added in the course of applying standard tableau rules to Gug. Thus, Gug can obviously be used for steering the non-deterministic decisions for Gns to construct a fully expanded and clash free completion graph if Gug is fully expanded and clash free.
Now, let Gns and Gug be completion graphs for Tns and Tug, respectively, and Gns and Gug coincide with the inferred facts so far, i.e., the conversion of concept facts and variable mappings from Gns corresponds to the contained concept facts in Gug. To show by induction that each rule application for Gns only adds concept facts and variable mappings, for which the conversion of these facts and variable mappings are also consequences in Gug, let 2; : : : ; ` be all possible variable mappings, i.e., f 2; : : : ; `g = compVTars(:CtD)(f g). Please note, it su ces to consider only the extended rules for concepts and axioms used for absorbing C v D, because only the concepts in aclosT (C v D) can be associated with variable mappings, for which the extended rules di er to standard rules.
First, we consider the 8-rule for a concept fact 8r:D0(v), 8r:D0 2 aclosT (C v D), which adds the concept fact D0(w) to an r-neighbour w of v in Gns and possibly the variable mapping cept fact D0(w) for cases where B(8r:D0; v) = ;, then mappGns (D0(w)) = f g (which is ensured by the absorption algorithm) and we have to show that in the completion graph Gug the concept facts (conv 2 (D0))(w); : : : ; (conv ` (D0))(w) are also added by rule applications. Obviously, this is the case, because the concept fact 8r:D0(v) 2 Bns(8r:D0; v) to Bns(D0; w). If the 8-rule only adds the concorresponds to (conv 2 (8r:D0))(v); : : : ; (conv ` (8r:D0))(v) in Gug and by applying the 8-rule for all concept facts (conv j (8r:D0))(v), 1 j `, we have the concepts conv 2 (D0); : : : ; conv ` (D0) in the label of all neighbour nodes. If the 8-rule adds a variable mapping 2 Bns(8r:D0; v) to Bns(D0; w), then we have to show that (conv 1 (D0))(w); : : : ; (conv k (D0))(w) with f 1; : : : ; kg = compVTars(:CtD)(f g) are added to Gug by rule applications. But this is also the case since 8r:D0(v) corresponds to (conv 1 (8r:D0))(w); : : : ; (conv k (8r:D0))(w) in Gug and applying the 8-rule for (conv 1 (8r:D0))(w); : : : ; (conv k (8r:D0))(w) adds (conv 1 (D0))(w); : : : ; (conv k (D0))(w) to the label of all neighbour nodes.
Next, we consider the v1-rule for an axiom H v D0 with H = A or H = fag and D0 , #x:D00 (we consider the addition of the binder concepts together with the #-rule). If Bns(H; v) = ; and the v1-rule adds only the concept fact D0(v) to a node, then we have to show that (conv 2 (D0))(v); : : : ; (conv ` (D0))(v) are also added to Gug by rule applications. Again, this is obviously the case, because for Gug we have the rules conv 2 (H) v conv 2 (D0); : : : ; conv ` (H) v conv ` (D0). If Bns(H; v) , ;, then H = A, the v1-rule adds also a variable mapping to Bns(D0; v) and we have to show that (conv 1 (D0))(v); : : : ; (conv k (D0))(v) with f 1; : : : ; kg = compVTars(:CtD)(f g) are added to Gug by rule applications. Again, this is a consequence of the concept facts (conv 1 (A))(v); : : : ; (conv k (A))(v) in Gug and the axioms conv 1 (A) v conv 1 (D0); : : : ; conv k (A) v conv k (D0) that we have to consider for Gug.
Let us now consider the v2-rule for an axiom (A1 u A2) v D0. If the v2-rule only adds the concept fact D0(v), then we have to show that (conv 2 (D0))(v); : : : ; (conv ` (D0))(v) are also added to Gug by rule applications. However, this is the case, because A1(v) and A2(v) corresponds to (conv j (A1))(v) and (conv j (A2))(v) in Gug, respectively, and, since we have the axiom (conv j (A1) u conv j (A2)) v conv j (D) for each 1 j `, it follows that all (conv 2 (D0))(v); : : : ; (conv ` (D0))(v) are also added to Gug. If the v2-rule also adds the variable mapping to Bns(D0; v), then we have to show that (conv 1 (D0))(v); : : : ; (conv k (D0))(v) with f 1; : : : ; kg = compVTars(:CtD)(f g) are also added to Gug by rule applications. Let us first assume that Bns(A1; v) = ; (Bns(A2; v) = ;). As a consequence, we have in Gug the concept facts (conv 2 (A2))(v); : : : ; (conv ` (A2))(v) and (conv 1 (A2))(v); : : : ; (conv k (A2))(v) ((conv 2 (A1))(v); : : : ; (conv ` (A1))(v) and (conv 1 (A1))(v); : : : ; (conv k (A1))(v)). As a consequence of the axioms (conv j (A1)uconv j (A2)) v conv j (D), for all 1 j `, the concept facts (conv 1 (D0))(v); : : : ; (conv k (D0))(v) are also added to Gug by rule applications. Let us now assume that Bns(A1; v) , ; as well as Bns(A2; v) , ;. We show that (conv 1 (D0))(v); : : : ; (conv k (D0))(v) has to be added to Gug, because (conv 1 (A1))(v); : : : ; (conv k (A1))(v) as well as (conv 1 (A2))(v); : : : ; (conv k (A2))(v) are in Gug. Obviously, there exists the variable mappings 0 2 Bns(A1; v) and 00 2 Bns(A2; v) with = dom( 0)[dom( 00) and for each x 2 (dom( 0)\dom( 00)) it holds that 0(x) = 00(x). Thus, 0 and 00 and as a consequence of the completion of 0 and 00 it follows that f 1; : : : ; kg f 01; : : : ; 0kg and f 1; : : : ; kg f 010; : : : ; 0k0g. Therefore, (conv 1 (A1))(v); : : : ; (conv k (A1))(v) and (conv 1 (A2))(v); : : : ; (conv k (A2))(v) are at least also in Gug.
The #-rule for a concept fact #x:D0(a) adds D0 to the label of a and the
variable mapping fx 7! ag to Bns(D0; a). We have to show that the concept facts
> u conv 1 (D0); : : : ; fag v > u conv k (D0).
are also added to Gug by rule applications. But this is obviously the case,
because in Gug we have the concept facts (conv 1 (#x:D0))(a); : : : ; (conv k (#x:D0))(a),
which is nothing else than (> u conv 1 (D0))(a); : : : ; (> u conv k (D0))(a).
Furthermore, we have to show that (> u conv 1 (D0))(a); : : : ; (> u conv k (D0))(a) is added
to Gug, because, as a consequence of the axiom O v #x:D0, #x:D0(a) is added
to Gns. Obviously, this is the case, because for Gug we have the axioms fag v
The application of the gr-rule adds for a concept fact gr(D0)(v) and a (possibly
empty) variable mapping
f 1; : : : ; kg = compVTars(:CtD)(f g). We have to show that D[
The extended tableau algorithm is still terminating. This is due to the fact that the number of variable mappings is limited by the number of ABox individuals and the number of variables in axioms. Thus, blocking is ensured since the nodes in the completion graph can only be labelled with a limited number of concepts and only a limited number of variable mappings can be associated to these concepts.
terminating for absorbed TBoxes with nominal schema axioms.