Nominal Schema Absorption

1 Introduction

We address the problem of an efficient handling of so-called nominal schema axioms in tableau calculi for Description Logics (DLs). Nominal schemas have been introduced recently [Kr¨otzsch et al., 2011] as a feature for expressing arbitrary DL-safe rules (as specified in the W3C standards SWRL [Horrocks et al., 2004] or RIF [Kifer and Boley, 2010]) natively in DLs and, consequently, in OWL ontologies [OWL Working Group, 2009]. Hence, DLs with nominal schemas provide a unified basis for OWL and rules. Although some attempts (see, e.g., [Krisnadhi and Hitzler, 2012]) have been made to improve the performance of tableau calculi when extended with nominal schemas, handling of nominal schemas remains challenging. We tackle this problem by extending the well-know tableau optimisation of absorption [Horrocks and Tobies, 2000]. The resulting calculus extends a standard tableau calculus by additional rules to deal with the absorbed nominal schema axioms and shows encouraging performances in comparison to existing techniques.

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, Thorsten Liebig derivo GmbH Germany liebig@derivo.de e.g., the interpretation of the concept {a} consists of the element that represents the named individual a. Nominal schemas introduce a new concept constructor {x}, 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.

∗The first author acknowledges the support of the doctoral scholarship under the Postgraduate Scholarships Act of the Land of Baden-Wuerttemberg (LGFG).

We use the same running example as Krisnadhi and Hitzler (2012), which describes a conflicting review assignment for an individual who has to review a paper x that has an author y with whom that individual has a joint publication in the same venue z:

∃hasReviewAssignment.({x} ⊓ ∃hasAuthor.{y} ⊓ ∃atVenue.{z}) ⊓ ∃hasSubmittedPaper.(∃hasAuthor.{y} ⊓ ∃atVenue.{z}) hasConflictingAssignedPaper.{x}.

For brevity, we shorten hasReviewAssignment to r, hasAuthor to a, atVenue to v, hasSubmittedPaper 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, 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 inefficient. For example, a nominal schema axiom with 3 variables can be grounded for a knowledge base with 100 ABox individuals in 1003 different ways, which is prohibitive even for small examples.

A promising approach for efficient 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., [Horrocks et al., 2006]), which are dominantly used for sound and complete reasoning systems for expressive DLs. One such approach extends a tableau algorithm such that grounding is delayed until it is required [Krisnadhi and Hitzler, 2012]. However, this requires significant changes to the tableau algorithm and, thus, to existing optimisations, which are crucial for a reasonable performance on real-world ontologies. Furthermore, it is not clear in which way concepts have to be grounded to achieve a well-performing implementation and some concepts even cannot be grounded efficiently.

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 proofs are available in a technical report [Steigmiller et al., 2013].

2 Preliminaries

For brevity, we do not introduce DLs (see, e.g., [Baader et al., 2007]) and we only present our approach for ALCOIQV. Covering SROIQV is, however, easily possible: role chains (incl. transitivity) can be encoded [Horrocks et al., 2006] and the remaining SROIQ features are easy to support.

Model construction calculi, such as tableau, decide the consistency of a knowledge base K by trying to construct an abstraction of a model for K, a so-called "completion graph". A completion graph G is a tuple (V,E,L, ˙ ̸=), where each node x ∈ V (edge 〈x, y〉 ∈ E) represents one or more (pairs of) individuals. Each node x (edge 〈x, y〉) is labelled with a set of concepts (roles), L(x) (L(〈x, y〉)), which the individuals represented by x (〈x, y〉) are instances of. The relation ˙ ̸= records inequalities between nodes.

The algorithm works by initialising the graph 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). Complex concepts are then decomposed using a set of expansion rules, where each rule application can add new concepts to node labels and/or new nodes and edges to the completion graph, thereby explicating the structure of a model. The rules are applied until either the graph is fully expanded (no more rules are applicable), in which case the graph can be used to construct a model that is a witness to the consistency of K, or an obvious contradiction (called a clash) is discovered (e.g., both C and ¬C in a node label), proving that the completion graph does not correspond to a model. The input knowledge base K is consistent if the rules (some of which are non-deterministic) can be applied such that they build a fully expanded, clash free completion graph.

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 ⊑ D, whether C is satisfied for a node v and only then adds D to L(v). If C is complex, it can, however, be non-trivial to decide whether C is satisfied for v. To guarantee correctness, one treats axioms where C is complex as ⊤ ⊑ ¬C ⊔D. Given that ⊤ is satisfied at each node, the disjunction 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 ⊤ ⊑ ¬C ⊔ D.

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 ∃r.(A1 ⊔ A2) ⊑ ∃s.A as ⊤ ⊑ ∀r.(¬A1 ⊓ ¬A2) ⊔ ∃s.A. Any node that does not have an r-neighbour trivially satisfies ∀r.(¬A1 ⊓¬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 ∃s.A. Hence, the disjunctive axiom can be rewritten into A1 ⊑ T, A2 ⊑ T and T ⊑ ∀r-.(∃s.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 ∀r.(¬A1 ⊓ ¬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.

For a more complex absorption it is often necessary to join several conditions, say A1 to An. An efficient way to do this is binary absorption [Hudek and Weddell, 2006], where two concepts A1 and A2 imply a fresh atomic concept T1 by the axiom (A1 ⊓ A2) ⊑ T1. We can then combine T1 with the next condition A3 and so on, until (Tn-2 ⊓ An) ⊑ Tn-1, where Tn-1 can then be used for further absorption.

3 Absorption Algorithm

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 ∃r.(A ⊓ ∀r.C) ⊑ D is, without absorption, handled as ⊤ ⊑ ∀r.(¬A⊔∃r.¬C)⊔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 ⊑ ∀r-.(∀r.(¬A ⊔ ∃r.¬C) ⊔ 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 ′ :

• isCA(C) (isPA(C)) is a recursive function that returns true if the concept C is completely (partially) absorbable and false otherwise. For the base case, C is completely (partially) absorbable if C has the form ¬{a} or ¬A (¬{a}, ¬A, or ∀r.C ′ ). For the recursion, C is completely absorbable if

Algorithm 1 collectDisjuncts(C, absorbable), returns the absorbable/not absorbable disjuncts of the concept C

1: S ← {C} 2: while (C1 ⊔C2) ∈ S do 3: S ← (S \ (C1 ⊔C2)) ∪ {C1,C2} 4: end while 5: if absorbable = true then return { C ∈ S | isPA(C) } 6: else return { C ∈ S | ¬isCA(C) } 7: end if

Algorithm 2 absorbJoined(S), returns the atomic concept that is implied by the join of the absorptions of S

1: S′ ← ∅ 2: for all C ∈ S do 3: A′ ←absorbConcept(C) 4: S′ ←S′ ∪ {A′} 5: end for 6: while A1 ∈ S′ and A2 ∈ S′ and A1 ̸= A2 do 7: T ← fresh atomic concept 8: T ′ ← T ′ ∪ {(A1 ⊓A2) ⊑ T} 9: S′ ← (S′ ∪ {T}) \ {A1,A2} 10: end while 11: if S′ = ∅ then return ⊤ 12: else return the element A′ ∈ S′ ▷ S′ is a singleton 13: end if

• C = ∀r.C ′ and C ′ is completely absorbable,
• either C = C1 ⊔ C2 or C = C1 ⊓ C2 and both C1 and C2 are completely absorbable;

and C is partially absorbable if

• C = C1⊔C2 and C1 or C2 are partially absorbable,
• C = C1 ⊓ C2 and both C1 and C2 are partially absorbable.

In all other cases, we say that C is neither completely nor partially absorbable, however, the absorption can further be extended to other constructors, e.g., to constructors of more expressive DLs [Steigmiller et al., 2013].

• collectDisjuncts(C, absorbable), shown in Algorithm 1, returns the set of (completely or partially) absorbable disjuncts for C if absorbable = true and the set of not completely absorbable disjuncts otherwise. If C is not a disjunction, then {C} itself is returned, in case it conforms to the specified absorbable condition.

For simplicity, we assume here that axioms of the form C ≡ D are rewritten into C ⊑ D and D ⊑ C. An extension that directly and, hence, more efficiently handles axioms of the form A ≡ C is also possible [Steigmiller et al., 2013].

To absorb the TBox T , we call for each axiom C ⊑ D the function absorbJoined for the set of absorbable disjuncts, i.e., collectDisjuncts(nnf(¬C ⊔ 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⊔ D), false). The methods absorbJoined (Algorithm 2) and absorbConcept (Algorithm 3) are recursively calling each other, whereby absorbJoined is joining several atomic concepts with binary absorption axioms and absorbConcept cre- Algorithm 3 absorbConcept(C), returns the atomic concept for the absorption of the concept C

1: if C = C1 ⊓C2 then 2: A1 ←absorbJoined(collectDisjuncts(C1, true)) 3: A2 ←absorbJoined(collectDisjuncts(C2, true)) 4: T ← fresh atomic concept 5: T ′ ← T ′ ∪ {A1 ⊑ T,A2 ⊑ T} 6: return T 7: else if C = ∀r.C ′ then 8: Anb ←absorbJoined(collectDisjuncts(C′ , true)) 9: T ← fresh atomic concept 10: T ′ ← T ′ ∪ {Anb ⊑ ∀r-.T} 11: return T 12: else if C = ¬{a} then 13: T ← fresh atomic concept 14: T ′ ← T ′ ∪ {{a} ⊑ T} 15: return T . . . 16: else return A ▷ C is of the form ¬A 17: end if

ates the absorption for a specific concept. For instance, a concept of the form ∀r.C can be absorbed (lines 7-11 of Algorithm 3) by creating a propagation from the atomic concept Anb, which is obtained by the absorption of the concept 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 ⊤ ⊑ ∀r-.T is created, which corresponds to ∃r.⊤ ⊑ T and, thus, is similar to the well known role absorption [Tsarkov and Horrocks, 2004].

The absorbJoined function creates binary absorption axioms (Algorithm 2, lines 6-10) 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:

Theorem 1 Let T denote a TBox, T ′ the TBox obtained by absorbing T , and C a concept, then C is satisfiable with respect to T iff it is satisfiable with respect to T ′ .

4 Nominal Schema Absorption

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 [Forgy, 1982], are used naively. Our approach to overcome this issue is to emulate such rule processing mechanisms by adapted tableau rules, which propagate bindings of variables for concepts through the completion graph. As a nice side-effect, this propagation means that complex roles can be supported without further adjustments. Analogously to ordinary GCIs, our approach works well if the axioms with nominal schemas have a large absorbable part and, furthermore, most nominal schema variables appear at least once in the absorbable part.

4.1 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⊓C2 in an absorbable disjunct, where different 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 ⊓ C2 once with C1 and once with C2. For example, the axiom {x} ⊔ A ⊑ ∃r.{x} is handled as the disjunction (¬{x}⊓¬A)⊔∃r.{x} in the absorption and to eliminate ¬{x} ⊓ ¬A we replace the original axiom with {x} ⊑ ∃r.{x} and A ⊑ ∃r.{x}.

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 ¬{x} is completely (partially) absorbable.
• absorbConcept(C) of Algorithm 3 must now also handle a negated occurrence of a nominal schema ¬{x} by absorbing it to O ⊑ ↓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 [Blackburn and Tzakova, 1998], is introduced to actually bind variables to individuals (or nodes in a completion graph). It is handled by a new tableau rule, which adds, for a node a with ↓x.Tx ∈ L(a), Tx to the label and records that x is bound to a. In the remainder, we assume that knowledge bases contain, for each individual a, an axiom of the form {a} ⊑ 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 ⊑ ↓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 remaining, non-absorbed part of the axiom, say the disjuncts D1, . . . ,Dn, have to be added with a disjunction that is grounded with those bindings of variables that have been propagated to the last concept from the absorption, say 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 ⊑ gr(D1 ⊔ . . . ⊔ 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.

completely absorbed into the following axioms:

where Tx, Ty, Tz, T1, . . . , T7 are fresh atomic concepts. Only ∃c.{x} 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 ¬{y} and ¬{z} a separate binder concept.

4.2 Tableau AlgorithmExtensions

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 ⊑1-rule handles GCIs of the form A ⊑ C (i.e., a non-absorbable axiom C ⊑ D is handled as ⊤ ⊑ nnf(¬C⊔D)) and the ⊑2-rule handles binary absorption axioms of the form (A1 ⊓ A2) ⊑ C. These rules and the ∀-rule (for transitivity support also the ∀+-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 in-

stead of variable mapping in the remainder.

Figure 1: Variable mapping propagation example

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 ⊑1-rule to an axiom of the form A ⊑ 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 ⊑2-rule that handles binary absorption axioms of the form (A1⊓A2) ⊑ 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 ✶ with the superscript ϵ.

Definition 2 (Variable Mapping Join) Two variable mappings µ1 and µ2 are compatible if µ1(x) = µ2(x) for all x ∈ dom(µ1) ∩ dom(µ2). For compatible mappings µ1 and µ2, µ1 ∪ µ2 is defined as (µ1 ∪ µ2)(x) = µ1(x) if x ∈ dom(µ1), and (µ1 ∪ µ2)(x) = µ2(x) otherwise. Given two (possibly empty) sets of variable mappings M1, M2, let M ϵ 1 = {ϵ} (M ϵ 2 = {ϵ}) if M1 = ∅ (M2 = ∅) and M ϵ 1 =M1 (M ϵ 2 = M2) otherwise. The join M1 ✶ϵ M2 is defined as {µ1 ∪ µ2 | µ1 ∈ M ϵ 1 , µ2 ∈ M ϵ 2 and µ1 is compatible with µ2} \ {ϵ}.

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

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) = ∅. Let µ be a variable mapping. We write C[µ] to denote the concept obtained by replacing each nominal schema {x} that occurs in C and x ∈ dom(µ) with the nominal {µ(x)}.

Given a set of variables Y and a variable mapping set M with M ϵ as the extension by the empty mapping ϵ if M = ∅, the completion compKY (M) of M w.r.t. Y and a knowledge base K containing the individuals Inds(K) is

The unrestricted application of generating rules such as the ∃-rule can lead to the introduction of infinitely many new tableau nodes. To guarantee termination, one uses a cycle detection technique called (pairwise) blocking [Horrocks and Sattler, 1999] that restricts the application of such rules. To apply blocking, we distinguish blockable nodes from nominal nodes, which have a nominal from the knowledge base in their label. A node v with predecessor v′ is blocked by a node w with predecessor w′ , if v, v′ ,w,w′ are all blockable and the labels of (i) v and w (ii) v′ and w′ and (iii) 〈v′ , v〉 and 〈w′ , w〉 coincide. We extend the standard blocking conditions to also require that the bindings for the concepts in the labels of these nodes coincide.

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. 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 {x ↦→ a1, y ↦→ a3, z ↦→ a4} is propagated to the grounding concept gr(∃c.{x}) ∈ L(a0) and, thus, by replacing the nominal schema {x} with the nominal {a1}, we have ∃c.{a1} 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.

Theorem 2 Let T denote an absorbed TBox (possibly with nominal schema axioms), then a tableau decision procedure (as described above) extended by the rules in Table 1 is a decision procedure for the satisfiability of T .

5 Implementation and Evaluation

The techniques are implemented in the novel reasoning system Konclude that supports SROIQV by (i) upfront grounding and (ii) tableau extensions with different optimisations.

A detailed evaluation can be found in the technical report [Steigmiller et al., 2013]. For brevity, we exemplarily show here some results for the University Ontology Benchmark (UOBM) [Ma et al., 2006] extended by DL-safe rules, which can straightforwardly be expressed as nominal schema axioms. This allows for comparing our system to the DL reasoners HermiT 1.3.7 1 and Pellet 2.3.0 [Sirin et al., 2007]. To the best of our knowledge, these are the only reasoning systems that support DL-safe rules for such expressive ontologies. The used ontology (UOBM1\D, data properties removed) has SHOIN expressivity and consists of 190, 093 axioms, 69 classes, 36 properties, and 25, 453 individuals. All experiments were performed on an Intel Core i7 940 quad core processor running at 2.93 GHz. The reasoners are restricted to use one core and all results are averaged over three runs. Exceeding the time limit of 24 hours is shown as time and the memory limit of 10 GB as mem in the results.

Table 2 shows the rules and the number of matches for each rule in the consistency check. However, since reasoning with UOBM-1 is non-deterministic, these numbers might vary between different 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 increase 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 [Kr¨otzsch et al., 2011]) it requires 647, 855, 209 new axioms. We have also implemented an optimisation where we create a representative for a set of variable mappings. Only these representatives are then propagated and considered in the dependency directed backtracking, which saves memory. The direct propagation and the propagation of representatives are depicted (i) with and (ii) without the backward chaining (BC) optimisation, which is used to restrict the creation and propagation of variable mappings, i.e., variable mappings are only created if there is an opportunity to propagate them to a grounding concept. This is realised by additionally absorbing nominal schema axioms, where all nominal schemas are replaced by O, and by using the created atomic concept from the absorption to identify "interesting" individuals with possibly the grounding concept in the label. We then use a back propagation, whereby only binder concepts are activated that are in the scope of these "interesting" individuals. However, for example for rule R2, still nearly all variable mappings have to be created and propagated, and thus, the backward chaining only slightly improves the reasoning time.

1 http://www.hermit-reasoner.com

Table 3 further shows the reasoning time increase for HermiT and Pellet when a rule from Table 2 is added. Without rules our system 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 our system 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 Conclusions

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.