A Tableaux Decision Procedure for SHOIQ

1 Introduction

Description Logics (DLs) are a family of logic based knowledge representation formalisms. Although they have a range of applications (e.g., configuration [McGuinness&Wright, 1998], and information integration [Calvanese et al., 1998]), they are perhaps best known as the basis for widely used ontology languages such as OIL, DAML+OIL and OWL [Horrocks et al., 2003], the last of which is now a W3C recommendation [Bechhofer et al., 2004]. Two of the three language "species" described in the OWL specification are based on expressive DLs: OWL Lite is based on SHIF, and OWL DL is based on SHOIN. This decision was motivated by a requirement that key inference problems (such as ontology consistency) be decidable, and that it should be possible to provide reasoning services to support ontology design and deployment [Horrocks et al., 2003].

Although the ontology consistency problem for SHOIN is known to be decidable, 1 to the best of our knowledge no "practical" decision procedure is known for it, i.e., no goal directed procedure that is likely to perform well with realistic ontology derived problems [Tobies, 2001; Horrocks & Sattler, 2001]. In this paper we present such a decision procedure for SHOIQ, i.e., SHOIN extended with qualified number restrictions [Baader&Hollunder, 1991]. The algorithm extends the well-known tableaux algorithm for SHIQ [Horrocks et al., 1999], which is the basis for several highly successful implementations [Horrocks&Patel-Schneider, 1998; Haarslev&M¨oller, 2001; Pellet, 2003].

The O in SHOIQ denotes nominals, i.e., classes with a singleton extension. Nominals are a prominent feature of hybrid logics [Blackburn&Seligman, 1995], and can also be viewed as a powerful generalisation of ABox individuals [Schaerf, 1994; Horrocks&Sattler, 2001]. They occur naturally in ontologies, e.g., when describing a class such as EUCountries by enumerating its members, i.e., {Austria, . . . ,UnitedKingdom} (such an enumeration is equivalent to a disjunction of nominals). This allows applications to infer, e.g., that persons who only visit EUCountries can visit at most 15 countries.

1 This is an immediate consequence of a reduction of DLs with transitive roles to DLs without such roles [Tobies, 2001] and the fact that applying this reduction to SHOIN yields a fragment of the two variable fragment of first order logic with counting quantifiers [Pacholski et al., 1997].

One reason why DLs (and propositional modal and dynamic logics) enjoy good computational properties, such as being robustly decidable, is that they have some form of tree model property [Vardi, 1997], i.e., if an ontology is consistent, then it has a (form of) tree model. This feature is crucial in the design of tableaux algorithms, allowing them to search only for tree like models. More precisely, tableaux algorithms decide consistency of an ontology by trying to construct an abstraction of a model for it, a so-called "completion graph". For logics with the tree model property, we can restrict our search/construction to tree-shaped completion graphs.

Tableaux algorithms for expressive DLs employ a cycle detection technique called blocking to ensure termination. This is of special interest for SHIQ, where the interaction between inverse roles and number restrictions results in the loss of the finite model property, i.e., there are consistent ontologies that only admit infinite models. On such an input, the SHIQ tableaux algorithm generates a finite tree-shaped completion graph that can be unravelled into an infinite tree model, and where a node in the completion graph may stand for infinitely many elements of the model. Even when the language includes nominals, but excludes one of number restrictions or inverse roles [Horrocks&Sattler, 2001; Hladik&Model, 2004], or if nominals are restricted to ABox individuals [Horrocks et al., 2000], we can work on forestshaped completion graphs, with each nominal (individual) being the root of a tree-like section; this causes no inherent difficulty as the size of the non-tree part of the graph is restricted by the number of individuals/nominals in the input.

The difficulty in extending the SHOQ or SHIQ algorithms to SHOIQ is due to the interaction between nominals, number restrictions, and inverse roles, which leads to the almost complete loss of the tree model property, and causes the complexity of the ontology consistency problem to jump from ExpTime to NExpTime [Tobies, 2000]. To see this, consider an ontology containing the following two axioms that use a nominal o to impose an upper bound, say 17, on the number of instances of the concept F:

The first statement requires that, in a model of this ontology, every element has an incoming R-edge from o; the second statement restricts the number of R-edges going from o to instances of F to at most 17. In this case, we might need to consider arbitrarily complex relational structures amongst instances of F, and thus cannot restrict our attention to completion trees or forests. Let us assume that our ontology also forces the existence of an infinite number of instances of another concept, say N, which requires the above mentioned "block and unravel" technique. The consistency of the whole ontology then crucially depends on the relations enforced between instances of F and N, and whether the unravelling of the N-part violates atmost number restrictions that instances of F must satisfy. Summing up, a tableaux algorithm for SHOIQ needs to be able to handle both arbitrarily complex relational structures and finite tree structures representing infinite trees, and to make sure that all constraints are satisfied (especially number restrictions on relations between these two parts), while still guaranteeing termination.

Two key intuitions have allowed us to devise a tableaux algorithm that meets all of these requirements. The first intuition is that, when extending a SHOIQ completion graph, we can distinguish those nodes that may be arbitrarily interconnected (so-called nominal nodes) from those nodes that still form a tree structure (so-called blockable nodes). Fixing a (double exponential) upper bound on the number of nominal nodes is crucial to proving termination; it is not, however, enough to guarantee termination, as we may repeatedly create and merge nominal nodes (a so-called "yo-yo").

The second intuition is that the yo-yo problem can be overcome by "guessing" the exact number of new nominal nodes resulting from interactions between existing nominal nodes, inverse roles, and number restrictions. This guessing is implemented by a new expansion rule, Ro?, which, when applied to a relevant (⩽nR.C) concept, generates (nondeterministically) between 1 and n new nominal nodes, all of which are pairwise disjoint. This prevents the repeated yo-yo construction, and termination is now guaranteed by the upper bound on the number of nominal nodes and the use of standard blocking techniques for the blockable nodes. The nondeterminism introduced by this rule could clearly be problematical for large values of n, but large values in number restrictions are already known to be problematical for SHIQ. Moreover, the rule has excellent "pay as you go" characteristics: in case number restrictions are functional (i.e., where n is 1), 2 the new rule becomes deterministic; in case there are no interactions between number restrictions, inverse roles and nominals, the rule will never be applied; in case there are no nominals, the new algorithm will behave like the algorithm for SHIQ; and in case there are no inverse roles, the new algorithm will behave like the algorithm for SHOQ.

For more examples and full proofs, we refer the reader to [Horrocks&Sattler, 2005].

2 A feature of many realistic ontologies; see, e.g., the DAML ontology library at http://www.daml.org/ontologies/

2 Preliminaries

In this section, we introduce the syntax, semantics, and inference problems of the DL SHOIQ.

Definition 1 Let R be a set of role names with both transitive and normal role names R+ ∪RP = R, where RP ∩R+ = ∅. The set of SHOIQ-roles (or roles for short) is R ∪ {R- | R ∈ R}. A role inclusion axiom is of the form R ⊑ S, for two roles R and S. A role hierarchy is a finite set of role inclusion axioms.

An interpretation I = (∆I , ·I ) consists of a non-empty set ∆I , the domain of I, and a function ·I which maps every role to a subset of ∆I ×∆I such that, for P ∈ R and R ∈ R+,

An interpretation I satisfies a role hierarchy R if RI ⊆ SI for each R ⊑ S ∈ R; such an interpretation is called a model of R.

We introduce some notation to make the following considerations easier.

1. The inverse relation on roles is symmetric, and to avoid considering roles such as R--, we define a function Inv which returns the inverse of a role: for R ∈ R, Inv(R) := Rand Inv(R-) := R.
2. Since set inclusion is transitive and RI ⊆ SI implies Inv(R)I ⊆ Inv(S)I , for a role hierarchy R, we introduce ⊑* R as the transitive-reflexive closure of ⊑ on R∪{Inv(R) ⊑ Inv(S) | R ⊑ S ∈ R}. We use R ≡R S as an abbreviation for R ⊑* RS and S ⊑* RR.
3. Obviously, a role R is transitive if and only if its inverse Inv(R) is transitive. However, in cyclic cases such as R ≡R S, S is transitive if R or Inv(R) is a transitive role name. In order to avoid these case distinctions, the function Trans returns true if R is a transitive role-regardless whether it is a role name, the inverse of a role name, or equivalent to a transitive role name (or its inverse): Trans(S,R) := true if, for some P with P ≡R S, P ∈ R+ or Inv(P) ∈ R+; Trans(S,R) := false otherwise.
4. A role R is called simple w.r.t. R if Trans(S,R) = false for all S ⊑* RR.
5. In the following, if R is clear from the context, we may use ⊑* and Trans(S) instead of ⊑* R and Trans(S,R).
6. Definition 2 Let NC be a set of concept names with a subset NI ⊆ NC of nominals. The set of SHOIQ-concepts (or concepts for short) is the smallest set such that
7. every concept name C ∈ NC is a concept,
8. if C and D are concepts and R is a role, then (C ⊓ D), (C ⊔D), (¬C), (∀R.C), and (∃R.C) are also concepts (the last two are called universal and existential restrictions, resp.), and
9. if C is a concept, R is a simple role 3 and n ∈ IN, then (⩽nR.C) and (⩾nR.C) are also concepts (called atmost and atleast number restrictions).

3 Restricting number restrictions to simple roles is required in order to yield a decidable logic [Horrocks et al., 1999].

The interpretation function ·I of an interpretation I = (∆I , ·I ) maps, additionally, every concept to a subset of ∆I such that

where ♯M is the cardinality of a set M and RI (x,C) is defined as {y | 〈x, y〉 ∈ RI and y ∈ C I }.

For C andD (possibly complex) concepts, C ˙⊑D is called a general concept inclusion (GCI), and a finite set of GCIs is called a TBox.

An interpretation I satisfies a GCI C ˙⊑ D if C I ⊆ DI , and I satisfies a TBox T if I satisfies each GCI in T ; such an interpretation is called a model of T .

A concept C is satisfiable w.r.t. a role hierarchy R and a TBox T if there is a model I of R and T with C I ̸= ∅. Such an interpretation is called a model of C w.r.t. R and T . A concept D subsumes a concept C w.r.t. R and T (written C ⊑R,T D) if C I ⊆ DI holds in every model I of R and T . Two concepts C, D are equivalent w.r.t. R and T (written C ≡R,T D) if they are mutually subsuming w.r.t. R and T .

As usual, subsumption and satisfiability can be reduced to each other. Like SHIQ, in SHOIQ, we can reduce reasoning w.r.t. TBoxes and role hierarchies to reasoning w.r.t. role hierarchies only: we can use an "approximation" of a universal role to internalise a TBox [Horrocks et al., 1999; Horrocks&Sattler, 2005]. Hence, in the remainder of this paper, we restrict our attention without loss of generality to the satisfiability of SHOIQ concepts w.r.t. a role hierarchy.

Finally, we did not choose to make a unique name assumption, i.e., two nominals might refer to the same individual. However, the inference algorithm presented below can easily be adapted to the unique name case by a suitable initialisation of the inequality relation ̸ .= used in our algorithm.

3 A Tableau for SHOIQ

For ease of presentation, as usual, we assume all concepts to be in negation normal form (NNF). Each concept can be transformed into an equivalent one in NNF by pushing negation inwards, making use of de Morgan's laws and the duality between existential and universal restrictions, and between atmost and atleast number restrictions, [Horrocks et al., 2000]. For a concept C, we use ˙¬C to denote the NNF of ¬C, and we use sub(C) to denote the set of all subconcepts of C (including C). As usual, for a concept D and a role hierarchy R, we define the set of "relevant sub-concepts" cl(D,R) as follows (we will often use cl(D) instead of cl(D,R)):

Definition 3 If D is a SHOIQ-concept in NNF, R a role hierarchy, and RD is the set of roles occurring in D or R, together with their inverses, a tableau T for D w.r.t. R is defined to be a triple (S,L, E) such that: S is a set of individuals, L : S → 2cl(D) maps each individual to a set of concepts which is a subset of cl(D), E : RD → 2S×S maps each role in RD to a set of pairs of individuals, and there is some individual s ∈ S such that D ∈ L(s). For all s, t ∈ S, C, C1, C2 ∈ cl(D), R, S ∈ RD, and

it holds that:

• (P1) if C ∈ L(s), then ¬C /∈ L(s),
• (P2) if C1 ⊓C2 ∈ L(s), then C1 ∈ L(s) and C2 ∈ L(s),
• (P3) if C1 ⊔C2 ∈ L(s), then C1 ∈ L(s) or C2 ∈ L(s),
• (P4) if ∀R.C ∈ L(s) and 〈s, t〉 ∈ E(R), then C ∈ L(t),
• (P5) if ∃R.C ∈ L(s), then there is some t ∈ S such that 〈s, t〉 ∈ E(R) and C ∈ L(t),
• (P6) if ∀S.C ∈ L(s) and 〈s, t〉 ∈ E(R) for some R⊑* S with Trans(R), then ∀R.C ∈ L(t),
• (P7) if (⩾nS.C) ∈ L(s), then ♯S T(s,C) ⩾ n,
• (P8) if (⩽nS.C) ∈ L(s), then ♯S T(s,C) ⩽ n,
• (P9) if (⩽nS.C) ∈ L(s) and 〈s, t〉 ∈ E(S), then {C, ˙¬C}∩ L(t) ̸= ∅,
• (P10) if 〈s, t〉 ∈ E(R) and R⊑* S, then 〈s, t〉 ∈ E(S),
• (P11) 〈s, t〉 ∈ E(R) iff 〈t, s〉 ∈ E(Inv(R)), and
• (P12) if o ∈ L(s) ∩L(t) for some o ∈ NI , then s = t.

Lemma 4 A SHOIQ-concept D in NNF is satisfiable w.r.t. a role hierarchy R iff D has a tableau w.r.t. R.

The proof is similar to the one found in [Horrocks et al., 1999]. Roughly speaking, we construct a model I from a tableau by taking S as its interpretation domain and adding the missing role-successorships for transitive roles. Then, by induction on the structure of formulae, we prove that, if C ∈ L(s), then s ∈ C I . Most cases are straightforward. As for SHIQ, (P7) and (P8) together with the fact that only simple roles occur in number restrictions ensure that this implication holds for number restrictions C, and (P12) ensures that nominals are indeed interpreted as singletons. For the converse, we can easily transform any model into a tableau.

4 A tableau algorithm for SHOIQ

From Lemma 4, an algorithm which constructs a tableau for a SHOIQ-concept D can be used as a decision procedure for the satisfiability of D with respect to a role hierarchy R. Such an algorithm will now be described in detail.

Definition 5 Let R be a role hierarchy and D a SHOIQconcept in NNF. A completion graph for D with respect to R is a directed graph G = (V, E, L, ̸ .=) where each node x ∈ V is labelled with a set L(x) ⊆ cl(D) ∪ NI ∪ {(⩽mR.C) | (⩽nR.C) ∈ cl(D) and m ≤ n} and each edge 〈x, y〉 ∈ E is labelled with a set of role names L(〈x, y〉) containing (possibly inverse) roles occurring in D or R. Additionally, we keep track of inequalities between nodes of the graph with a symmetric binary relation ̸ .= between the nodes of G.

If 〈x, y〉 ∈ E, then y is called a successor of x and x is called a predecessor of y. Ancestor is the transitive closure of predecessor, and descendant is the transitive closure of successor. A node y is called an R-successor of a node x if, for some R′ with R′ ⊑* R, R′ ∈ L(〈x, y〉); x is called an R-predecessor of y if y is an R-successor of x. A node y is called a neighbour (R-neighbour) of a node x if y is a successor (R-successor) of x or if x is a successor (Inv(R)- successor) of y.

For a role S and a node x in G, we define the set of x's S-neighbours with C in their label, S G(x, C), as follows:

• SG(x, C) := {y | y is an S-neighbour of x and C ∈ L(y)}.

G is said to contain a clash if

1. for some A ∈ NC and node x of G, {A, ¬A} ⊆ L(x),
2. for some node x of G, (⩽nS.C) ∈ L(x) and there are n + 1 S-neighbours y0, . . . , yn of x with C ∈ L(yi) for each 0 ≤ i ≤ n and yi ̸ .= yj for each 0 ≤ i < j ≤ n, or
3. for some o ∈ NI , there are x ̸ .= y with o ∈ L(x)∩L(y).

If o1, . . . , oℓ are all the nominals occurring in D, then the tableau algorithm starts with the completion graph G = ({r0, r1 . . . , rℓ}, ∅,L, ∅) with L(r0) = {D} and L(ri) = {oi} for 1 ≤ i ≤ ℓ. G is then expanded by repeatedly applying the expansion rules given in Figures 1 and 2, stopping if a clash occurs.

Next, we define and explain some terms and operations used in the expansion rules:

Nominal Nodes and Blockable Nodes We distinguish two types of nodes in G, nominal nodes and blockable nodes. A node x is a nominal node if L(x) contains a nominal. A node that is not a nominal node is a blockable node. A nominal o ∈ NI is said to be new in G if no node in G has o in its label.

Comment: like ABox individuals [Horrocks et al., 2000], nominal nodes can be arbitrarily interconnected. In contrast, blockable nodes are only found in tree-like structures rooted in nominal nodes (or in r0); a branch of such a tree may end with an edge leading to a nominal node.

In Ro?, we use new nominals to create new nominal nodes-intuitively, to fix the identity of certain, constrained neighbours of nominal nodes. An upper bound on the number of nominal nodes that can be generated in a given completion graph will be crucial for termination of the construction, given that blocking cannot be applied to nominal nodes.

Blocking A node x is label blocked if it has ancestors x′ , y and y′ such that

1. x is a successor of x′ and y is a successor of y′ ,
2. y, x and all nodes on the path from y to x are blockable,
3. L(x) = L(y) and L(x′ ) = L(y′ ), and
4. L(〈x′ , x〉) = L(〈y′ , y〉).

In this case, we say that y blocks x. A node is blocked if either it is label blocked or it is blockable and its predecessor is blocked; if the predecessor of a blockable node x is blocked, then we say that x is indirectly blocked.

Comment: blocking is defined exactly as for SHIQ, with the only difference that, in the presence of nominals, we must

• R⊓: if 1. C1 ⊓C2 ∈ L(x), x is not indirectly blocked, and 2. {C1,C2} ̸⊆ L(x)

then set L(x) = L(x) ∪ {C1, C2}

• R⊔: if 1. C1 ⊔C2 ∈ L(x), x is not indirectly blocked, and 2. {C1, C2} ∩ L(x) = ∅ then set L(x) = L(x) ∪ {C} for some C ∈ {C1, C2}
• R∃: if 1. ∃S.C ∈ L(x), x is not blocked, and 2. x has no safe S-neighbour y with C ∈ L(y), then create a new node y with L(〈x, y〉) = {S} and L(y) = {C}
• R∀: if 1. ∀S.C ∈ L(x), x is not indirectly blocked, and 2. there is an S-neighbour y of x with C /∈ L(y) then set L(y) = L(y) ∪ {C}
• R∀+: if 1. ∀S.C ∈ L(x), x is not indirectly blocked, and 2. there is some R with Trans(R) and R ⊑* S, 3. there is an R-neighbour y of x with ∀R.C /∈ L(y) then set L(y) = L(y) ∪ {∀R.C}
• R?: if 1. (⩽nS.C) ∈ L(x), x is not indirectly blocked, and there 2. is an S-neighbour y of x with {C, ˙¬C} ∩L(y) = ∅ then set L(y) = L(y) ∪ {E} for some E ∈ {C, ˙¬C}
• R⩾: if 1. (⩾nS.C) ∈ L(x), x is not blocked, and 2. there are not n safe S-neighbours y1, . . . , yn of x with C ∈ L(yi) and yi ̸ .= yj for 1 ≤ i < j ≤ n then create n new nodes y1, . . . , yn with L(〈x, yi〉) = {S}, L(yi) = {C}, and yi ̸ .= yj for 1 ≤ i < j ≤ n.
• R⩽: if 1. (⩽nS.C) ∈ L(z), z is not indirectly blocked, and 2. ♯SG(z, C) > n and there are two S-neighbours x, y of z with C ∈ L(x) ∩ L(y), and not x ̸ .= y
• then 1. if x is a nominal node, then Merge(y, x) then Merge(x, y)
• else if y is a nominal node or an ancestor of x, 3. else Merge(y, x)

Figure 1: The tableaux expansion rules for SHIQ

take care that none of the nodes between a blocking and a blocked one is a nominal node.

Generating and Shrinking Rules and Safe Neighbours

The rules R⩾, R∃, and Ro? are called generating rules, and the rules R⩽ and Ro are called shrinking rules. An Rneighbour y of a node x is safe if (i) x is blockable or if (ii) x is a nominal node and y is not blocked.

Pruning When a node y is merged into a node x, we "prune" the completion graph by removing y and, recursively, all blockable successors of y. More precisely, pruning a node y (written Prune(y)) in G = (V, E, L, ̸ .=) yields a graph that is obtained from G as follows:

1. for all successors z of y, remove 〈y, z〉 fromE and, if z is blockable, Prune(z);
2. remove y from V .

Merging merging a node y into a node x (written Merge(y, x)) in G = (V,E,L, ̸ .=) yields a graph that is obtained from G as follows:

1. for all nodes z such that 〈z, y〉 ∈ E
2. (a) if {〈x, z〉, 〈z, x〉}∩E = ∅, then add 〈z, x〉 toE and set L(〈z, x〉) = L(〈z, y〉),
3. (b) if 〈z, x〉 ∈ E, then set L(〈z, x〉) = L(〈z, x〉) ∪ L(〈z, y〉),
4. (c) if 〈x, z〉 ∈ E, then set L(〈x, z〉) = L(〈x, z〉) ∪ {Inv(S) | S ∈ L(〈z, y〉)}, and
5. (d) remove 〈z, y〉 fromE;
6. for all nominal nodes z such that 〈y, z〉 ∈ E
7. (a) if {〈x, z〉, 〈z, x〉}∩E = ∅, then add 〈x, z〉 toE and set L(〈x, z〉) = L(〈y, z〉),
8. (b) if 〈x, z〉 ∈ E, then set L(〈x, z〉) = L(〈x, z〉) ∪ L(〈y, z〉),
9. (c) if 〈z, x〉 ∈ E, then set L(〈z, x〉) = L(〈z, x〉) ∪ {Inv(S) | S ∈ L(〈y, z〉)}, and
10. (d) remove 〈y, z〉 fromE;
11. set L(x) = L(x) ∪L(y);
12. add x ̸ .= z for all z such that y ̸ .= z; and
13. Prune(y).

If y was merged into x, we call x a direct heir of y, and we use being an heir of another node for the transitive closure of being a "direct heir".

Comment: merging is a generalisation of what is often done to satisfy an atmost number restriction for a node x in case that x has too many neighbours. In SHOIQ, we might need to merge nominal nodes that are related in some arbitrary, non-tree-like way, so we must take care of all incoming and outgoing edges. The usage of "heir" is quite intuitive since, after y has been merged into x, x has "inherited" all of y's properties, i.e., its label, its inequalities, and its incoming and outgoing edges (except for any outgoing edges to blockable nodes, which are removed by Prune).

Level (of Nominal Nodes) Let o1, . . . , oℓ be all the nominals occurring in the input concept D. We define the level of a nominal node y inductively as follows: (i) each (nominal) node x with an oi ∈ L(x), 1 ≤ i ≤ ℓ, is of level 0, and (ii) a nominal node x is of level i if x is not of some level j < i and x has a neighbour that is of level i - 1.

Comment: if a node with a lower level is merged into another node, the level of the latter node may be reduced, but it can never be increased because Merge preserves all edges connecting nominal nodes. The completion graph initially contains only level 0 nodes.

Strategy (of Rule Application) the expansion rules are applied according to the following strategy:

1. Ro is applied with highest priority.
2. Next, R⩽ and Ro? are applied, and they are applied first to nominal nodes with lower levels. In case they are both applicable to the same node, Ro? is applied first.
3. All other rules are applied with a lower priority.

Comment: this strategy is necessary for termination, and in particular to fix an upper bound on the number of applications of Ro?.

We can now finish the description of the tableau algorithm: A completion graph is complete if it contains a clash, or when none of the rules is applicable. If the expansion rules can be applied to D and R in such a way that they yield a complete and clash-free completion graph, then the algorithm returns "D is satisfiable w.r.t. R", and "D is unsatisfiable w.r.t. R" otherwise.

• Ro: if for some o ∈ NI there are 2 nodes x, y with o ∈ L(x) ∩ L(y) and not x ̸ .= y then Merge(x, y)
• Ro?: if 1. (⩽nS.C) ∈ L(x), x is a nominal node, and there is a blockable S-neighbour y of x such that C ∈ L(y) and x is a successor of y
• there is no m with 1 ⩽ m ⩽ n, (⩽mS.C) ∈ L(x), and there are m nominal S-neighbours z1, . . . , zm of
• L(〈x, yi〉) = {S}, L(yi) = {C, oi} for oi ∈ NI new in G, and yi ̸ .= yj for 1 ≤ i < j ≤ m,

x with C ∈ L(zi) and yi ̸ .= yj for all 1 ≤ i < j ≤ m. then 1. guess m ⩽ n and set L(x) = L(x) ∪ {(⩽mS.C)} 2. create m new nodes y1, . . . , ym with

Figure 2: The new expansion rules for SHOIQ

Lemma 6 Let D be a SHOIQ concept in NNF and R a role hierarchy.

1. When started with D and R, the completion algorithm terminates.
2. D has a tableau w.r.t. R if and only if the expansion rules can be applied to D and R such that they yield a complete and clash-free completion graph.

Proof (sketch): Let m = |cl(D)|, k the number of roles and their inverses in D and R, n the maximal number in atmost number restrictions, and o1, . . . , oℓ be all nominals occurring in D, and let λ := 22m+k .

Termination is a consequence of the usual SHIQ conditions (1 - 3 below) with respect to the blockable tree parts of the graph [Horrocks et al., 1999], plus the fact that there is a bound on the number of new nominal nodes that can be added to G by Ro? (4 below): (1) all but the shrinking rules strictly extend the completion graph by adding new nodes and edges or extending node labels, while neither removing nodes, edges, or elements from node labels; (2) new nodes are only added by the generating rules, and each of these rules is applied at most once for a given concept in the label of a given node x or its heirs; (3) the length of a path consisting entirely of blockable nodes is bounded by λ: this is due to the blocking condition and the fact that, if x is blockable, then L(x) ⊆ cl(D,R) and thus does not contain nominals; and (4) at most O(ℓ(mn)λ ) nominal nodes are generated.

To see (4), observe that Ro? can only be applied after a nominal oi, for i ≤ ℓ, has been added to the label of a blockable node x in a branch of one of the blockable "trees"; otherwise, a blockable node cannot have a nominal node as a successor. In this case, Ro will immediately merge x with an existing level 0 node, say ri. As a consequence of this merging, it is possible that the predecessor of x is merged into a nominal node n1 by R⩽ (due to the pruning part of merging, this cannot happen to a successor of x). By definition, n1 is of level 0 or 1. Repeating this argument, it is possible that all ancestors of x are merged into nominal nodes. However, as the maximum length of a sequence of blockable nodes is λ, blockable ancestors of x can only be merged into nominal nodes of level below λ. Given the preconditions of Ro?, this implies that we can only apply Ro? to nominal nodes of level below λ. This, together with (2) above and some counting, yields the bound of O(ℓ(mn)λ ).

The remainder of the proof is very similar to the SHIQ case. For the second claim in Lemma 6, for the "if" direction, we can obtain a tableau T = (S, L′ , E) from a complete and clash-free completion graph G by unravelling blockable "tree" parts of the graph as usual. For the "only if" direction, using a tableau T = (S,L′ , E) for D w.r.t. R to steer the non-deterministic rules R⊔, R?, R⩽, and Ro?, we can indeed construct a complete and clash-free graph. ✷

Since subsumption can be reduced to (un)satisfiability and SHOIQ can internalise general TBoxes, we have the following result.

Theorem 7 The SHOIQ tableau algorithm is a decision procedure for satisfiability and subsumption of SHOIQ concepts w.r.t. TBoxes and role hierarchies.

5 Discussion

We have presented what is, to the best of our knowledge, the first goal-directed decision procedure for SHOIQ (and so SHOIN). Given that SHOIQ is NExpTime-complete [Tobies, 2000], it is clear that, in the worst case, any decision procedure will behave very badly, i.e., not terminate in practice. However, the algorithm given here is designed to behave well in many typically encountered cases, and to exhibit a "pay as you go" behaviour: if an input TBox, role hierarchy, and concept do not involve any one of inverse roles, number restrictions, or nominals, then Ro? will not be applied, and the corresponding non-deterministic guessing is avoided. This is even true for inputs that do involve all of these three constructors, but only in a "harmless" way. Hence, our SHOIQ algorithm can be implemented to perform just as well on SHIQ knowledge bases as state-of-the-art DL reasoners for SHIQ [Horrocks &Patel-Schneider, 1998; Haarslev&M¨oller, 2001; Pellet, 2003]. To find out whether our algorithm can handle some non-trivial, "true" SHOIQ inputs, we are currently extending a highly optimised DL reasoner, FaCT++ [Tsarkov&Horrocks, 2004], to implement the algorithm described here.