Chan Le Duc
email: leduc@iut.univ-paris8.fr

Myriam Lamolle
email: lamolle@iut.univ-paris8.fr

Olivier Curé

An EXPSPACE Tableau-based Algorithm for SHOIQ

Keywords: Logics, Decision Procedures, Tableaux, Complexity {Earth} ∃isPartOf.{SolarSystem},

In this work, we propose a worst-case optimal algorithm for deciding consistency in the description logic SHOIQ. The construction of this algorithm is founded on the standard tableau-based method for SHOIQ and the technique used for designing a NEXPTIME algorithm for the two-variable fragment of first-order logic with counting quantifiers C 2 .

Introduction

The ontology language OWL-DL [START_REF] Patel-Schneider | Owl web ontology language semantics and abstract syntax[END_REF] is widely used to formalize semantic resources on the Semantic Web. This language is mainly based on the description logic SHOIQ which is known to be decidable [START_REF] Tobies | The complexity of reasoning with cardinality restrictions and nominals in expressive description logics[END_REF]. Recently, another expressive description logic, namely SROIQ [START_REF] Horrocks | The even more irresistible SROIQ[END_REF], has provided a logical base for OWL 2 which is an extension of OWL. An interesting feature of logics with nominals (denoted by O in SHOIQ and SROIQ) is that they allow for expressing relationships, represented as role instances, between two sets of individuals which are represented as nominals or standard concepts. Such sets of individuals can be finitely enumerable or infinite. For instance, we consider the following axioms:

Thing ∃isAttractedBy.{Earth}.

The former can be expressed by an ABox assertion. However, it would not be straightforward to use ABox assertions to represent the latter. As a result, a TBox with nominals is more expressive than a non-nominal TBox with an ABox since ABox assertions such as C(a), R(a, b) or a = b can be directly expressed as TBox axioms with nominals as follows: {a} C, {a} ∃R.{b}, {a} ¬{b}.

There were several works on the consistency problem of a SHOIQ knowledge base. These works have not only shown decidability and complexity of the problem but also led to develop and implement efficient systems for reasoning on OWL-based ontologies. A result in [START_REF] Tobies | The complexity of reasoning with cardinality restrictions and nominals in expressive description logics[END_REF] has shown that the consistency problem of a SHOIQ knowledge base is NEXPTIME-complete. Moreover, tableau-based algorithms presented in [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF] and [START_REF] Horrocks | The even more irresistible SROIQ[END_REF] for SHOIQ have been exploited to implement reasoners such as FaCT++ [START_REF] Tsarkov | FaCT++ description logic reasoner: System description[END_REF], Pellet [START_REF] Sirin | Pellet: a pratical owl-dl reasoner[END_REF], which inherit from the success of early Description Logic reasoners such as FaCT [10] and RACER [START_REF] Haarslev | Racer system description[END_REF].

In addition, there are several results which have provided worst-case optimal algorithms for Description Logics (DL) without nominal. The work in [START_REF] Ortiz | An automata-based algorithm for description logics around SRIQ[END_REF] has introduced the so-called ALCQIb + reg logic (capturing SRIQ [START_REF] Horrocks | The irresistible SRIQ[END_REF]) that allows for a rich set of operators on roles by which one can simulate role inclusion axioms. Based on an automata approach, a powerful tool to establish complexity results for DLs and modal logics ( [START_REF] Vardi | Automata-theoretic techniques for modal logics of programs[END_REF], [START_REF] Vardi | Reasoning about the past with two-way automata[END_REF]), this work has also proposed a worst-case optimal algorithm for the satisfiability problem in ALCQIb + reg . Another approach, namely resolutionbased, has been used in [START_REF] Hustadt | A Decomposition Rule for Decision Procedures by Resolutionbased Calculi[END_REF] to devise a practical and worst-case optimal algorithm for deciding concept satisfiability in SHIQ.

It has been shown that when nominals are added to these DLs the consistency problem is harder. In fact, the complexity jumps from EXPTIME-complete for SHIQ to NEXPTIME-complete for SHOIQ [START_REF] Tobies | The complexity of reasoning with cardinality restrictions and nominals in expressive description logics[END_REF]. The work in [START_REF] Kazakov | A Resolution-Based Decision Procedure for SHOIQ[END_REF] has indicated that when nominals are allowed in SHIQ, the resolution-based approach yields a triple exponential decision procedure for the consistency problem. The authors have also identified that the interaction between nominals, inverse roles and number restrictions makes termination more difficult to be achieved, and thus, is responsible for this hardness. Recently, [START_REF] Motik | Hypertableau reasoning for description logics[END_REF] has introduced a combination of the resolution-based approach with a tableau-based method. It yields an efficient algorithm for checking consistency of a SHOIQ + knowledge base, which is an extension of SHOIQ with role operators. This algorithm has been exploited to implement the HermiT reasoner [START_REF] Shearer | HermiT: A Highly-Efficient OWL Reasoner[END_REF].

The presence of nominals in SHOIQ or SHOIQ + makes tree-like structures for representing models more difficult to be maintained. As a consequence, the algorithms presented in [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF] and [START_REF] Motik | Hypertableau reasoning for description logics[END_REF] have employed non tree-like structures to represent models and adapted the blocking technique, which is a main tool to ensure termination for logics without nominal, such that it works again for the new structures. Moreover, the presence of nominals may trigger a merging process that starts by merging two nominal nodes and may propagate through at-most number restrictions. To deal with these issues, these algorithms have to introduce new expansion rules that may add new nominals in order to, on the one hand, isolate a non like-tree part consisting of nominal nodes from a tree-like part consisting of non nominal nodes, and on the other hand, avoid infinite sequences of "generating-merging".

Our approach is inspired from a technique that was employed by De Giacomo and Lenzerini in [4] to simulate a functional role in DLs by using constructors in PDL. Intuitively, this technique said that "for every state s of a model M if (≤ 1 a) holds in s and if there is a a-transition from s to t 1 and a a-transition from s to t 2 then t 1 and t 2 are equivalent". We can apply this technique to DL context as follows : if an individual d must satisfy a term such as (≤ 1 a) and d has two a-neighbors d 1 and d 2 then d 1 , d 2 have to satisfy the same set of semantic constraints, i.e. the label of d 1 is identical to that of d 2 . It leads us to develop a technique that replaces merging d 1 into d 2 with (i) propagating the label from one to another and (ii) memorizing that d 1 and d 2 could be collapsed to a single individual. In other terms, this new technique is founded on the fact that fusions of nodes triggered by merging nominal nodes can be replaced with governing a partitioning function for memorizing nodes that could be merged. As a consequence, it allows us to maintain tree-like structures for representing models without adding new nominals, and thus, the blocking technique can be reused over these tree-like structures to achieve termination.

In addition, to obtain an EXPSPACE tableau-based algorithm for SHOIQ, we use a technique that was proposed by Ian Pratt-Hartmann in [START_REF] Pratt-Hartmann | Complexity of the two-variable fragment with counting quantifiers[END_REF] to construct a NEX-PTIME algorithm for the logic C 2 including SHOIQ. Unlike the existing tableaubased algorithms, this technique does not explicitly build a graph for representing a model but it builds a structure, called a frame, from star-types each of which represents a set of individuals. A result from [START_REF] Pratt-Hartmann | Complexity of the two-variable fragment with counting quantifiers[END_REF] shows that a model of a C 2 knowledge base can be constructed from a frame tiled by well selected star-types.

The present paper is structured as follows. In the next section, we describe the logic SHOIQ and the consistency problem for a SHOIQ knowledge base. Section 3 provides an overview of recent tableau-based algorithms and their issues. This section gives also main arguments that show how these issues can be solved in our approach. In Section 4, we provide a definition of tableaux for SHOIQ. Section 5 describes in detail a 2EXPSPACE tableau-based algorithm for checking consistency of a SHOIQ knowledge base. An advantage of this algorithm is that a tree-like structure can be maintained to obtain termination. Section ?? transfers a result in [START_REF] Pratt-Hartmann | Complexity of the two-variable fragment with counting quantifiers[END_REF] from C 2 to SHOIQ. Based on these results, we propose a worst-case optimal algorithm for deciding consistency of a SHOIQ knowledge base. Finally, we discuss the results and future work.

The Description Logic SHOIQ

In this section, we present the syntax, the semantics and main inference problems of SHOIQ. We start by defining a role hierarchy and its semantics.

Definition 1 (role hierarchy) Let R be a non-empty set of role names and R + ⊆ R be a set of transitive role names. We use R I = {P -| P ∈ R} to denote a set of inverse roles. Each element of R ∪ R I is called a SHOIQ-role. We define a function R which returns R -if R ∈ R, and returns R if R ∈ R I . * A role hierarchy R is a finite set of role inclusion axioms R S where R and S are two SHOIQ-roles. A relation * is defined as the transitive-reflexive closure of on R ∪ {R S | R S ∈ R}. We define a function Trans(R) which returns true iff there is some Notice that the simplicity of roles which relies on the function Trans(•) plays a crucial role in guaranteeing decidability of SHIQ [START_REF] Horrocks | Practical reasoning for expressive description logics[END_REF]. The underlying idea is that if a role R is simple then it is sufficient to count "direct" R-neighbors t of an individual s, i.e. s, t ∈ R I for some interpretation I, in order to satisfy a restriction that bounds the number of R-neigbors of s. Since negation is allowed in the logic SHOIQ, unsatisfiability and subsumption w.r.t. (T , R) can be reduced to each other: C D iff C ¬D is unsatisfiable. In addition, we can reduce satisfiability of concepts to knowledge base consistency : C is satisfiable w.r.t. a knowledge base (T , R) iff (T ∪{o C}, R) is consistent where o is a new nominal. Thanks to these reductions, it suffices to study knowledge base consistency.

Q ∈ R + ∪ {P | P ∈ R + } such that Q * R. A role R is called simple w.
For the ease of construction, we assume all concepts to be in negation normal form (NNF), i.e., negation occurs only in front of concept names. Any SHOIQconcept can be transformed to an equivalent one in NNF by using DeMorgan's laws and some equivalences as presented in [START_REF] Horrocks | Practical reasoning for expressive description logics[END_REF]. According to [1], nnf(C) can be computed in polynomial time in the size of C. For a concept C, we denote the nnf of C by nnf(C) and the nnf of ¬C by ¬C Let D be an SHOIQ-concept in NNF. We define cl(D) to be the smallest set that contains all sub-concepts of D including D.

For a knowledge base (T , R), we define a set cl(T , R) as follows:

cl(T , R) = C D∈T cl(nnf(¬C D), R) where cl(E, R) = cl(E) ∪ { ¬C | C ∈ cl(E)} ∪ {∀S.C | (∀R.C ∈ cl(E), S * R) or ( ¬∀R.C ∈ cl(E), S * R)
where S occurs in T or R} ∪ (1)

{ mS.C | (≤ nS.C) ∈ cl(E), ∈ {≤, ≥}, 1 ≤ m ≤ n} (2)
We use R (T ,R) to denote the set of all role names occurring in T , R with their inverse.

The definition of cl(T , R) is inspired from the Fischer-Ladner closure that was introduced in [START_REF] Fischer | Propositional dynamic logic of regular programs[END_REF]. The closure cl(T , R) contains not only sub-concepts syntactically obtained from T but also sub-concepts that are semantically derived from T w.r.t. R. For instance, (i

) if ∀S.C is a sub-concept from T and R * S ∈ R then ∀R.C ∈ cl(T , R), or (ii) if (≤ nS.C) ∈ cl(T ) with n ≥ 1 then (≤ mS.C), (≥ mS.C) ∈ cl(T , R) for all 1 ≤ m ≤ n.
This means that cl(T , R) must be large enough to cover all sub-concepts which represent potential nondeterminisms. These extensions of cl(T , R) are anticipated for the construction of tableaux described in Section 4.

Related Work and Algorithm Overview

In this section, we discuss several related works that employ tableau-based approach to devise efficient algorithms for the consistency problem of a DL knowledge base. Next, we provide an overview of our algorithm and explain how it addresses the issues encountered in tableau-based algorithms for DLs with inverse roles, number restrictions and nominals.

Related Work

Donini and Massacci in [7] have provided a tableau-based algorithm for the logic ALC that runs in single exponential time. The authors have proposed an unusual strategy that allows for reusing unsatisfiable concepts that are already discovered in a branch. As a result, this strategy may help to reduce the tree expansion required by the main complexity sources : or-branching ( ) and and-branching ( ,∃, ∀) [5].

Goré and Nguyen in [START_REF] Goré | Exptime tableaux with global caching for description logics with transitive roles, inverse roles and role hierarchies[END_REF] have proposed for the logic SHI an exponential time algorithm that is based on a global caching method. Basically, to decide satisfiability of a concept X w.r.t. a SHI knowledge base, this algorithm starts by building a and/or graph with an initial node containing X. Each node of the graph is associated with a status sat or unsat. When a node is decided to be sat, this status will be propagated to ancestors. The construction terminates if all nodes are saturated, i.e. no rule is applicable. This strategy of construction allows for reusing both unsatisfiable and satisfiable concepts that are already discovered.

As far as we know, the algorithms developed in these works have not been implemented yet. Moreover, it is not straightforward to extend these algorithms to DLs with number restrictions and nominals.

Motik, Shearer and Horrocks in [START_REF] Motik | Hypertableau reasoning for description logics[END_REF] have recently introduced an algorithm that is founded on a hypertableau-based approach for the logic SHOIQ + (SHOIQ with role operators). First, this approach translates TBox axioms of a DL knowledge base into first-order formulae, the so-called DL-clauses. Next, it applies derivation rules to devise new ABox assertions until saturation (i.e. no new ABox assertion can be generated). To deal with nominals and achieve termination, this approach has introduced a new rule, called NI-rule, that adds implicitly new nominals to ABox. This rule makes a crucial impact on (i) maintaining the tree-like part enabling to reuse blocking technique on it, and (ii) avoiding infinite sequences of "generating-merging" caused by generating-terms ∃R.C, (≥ nR.C) and merging-terms (≤ nR.C) with nominals.

Horrocks and Sattler have presented in [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF] a tableau-based algorithm for the DL SHOIQ that relies on two structures: tableau and completion graph. Roughly speaking, a tableau represents a model of a knowledge base and it is possibly infinite. A tableau translates satisfiability of all given concept and role inclusion axioms into satisfiability of constraints imposed locally on each individual of the tableau.

To check consistency of a knowledge base, tableau-based algorithms try to build a completion graph whose finiteness is ensured by blocking technique. The underlying idea of blocking technique is to detect "loops" which are repeated tree-like pieces of a completion graph. As a result, this technique works only for tree-like structures on which we can define blocked and blocking nodes such that (i) each blocked node must have a blocking ancestor, and (ii) each node x between a blocking and blocked node may be duplicated infinitely without violating the semantic constraints imposed by concepts in the label of x. For this reason, tableau-based algorithms manage to "push" nominal nodes (i.e. nodes containing nominals in their label) outside from tree-like structures.

Our approach introduced in this paper relies on the tableau-based algorithm presented in [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF], from which we have learned the following characteristics of completion graphs for SHOIQ:

Two-part structure of completion graphs

A completion graph for SHOIQ is formed of nominal nodes whose label contains a nominal, and non-nominal nodes. Such a graph consists of two parts: the so-called non-tree part and tree-like part. The non-tree part contains nominal nodes which can be arbitrarily interconnected. Nevertheless, the tree-like part includes non-nominal nodes which form a set of tree-like structures rooted in a nominal node, i.e., each non-nominal node of this part has at most one predecessor and may have a nominal successor.

The border between two parts of the structure

The two-part structure of completion graphs for SHOIQ makes a crucial impact on behaviours of the tableau-based algorithm. To ensure termination of such an algorithm, (i) we reuse the usual blocking condition for the tree-like part, (ii) we have to control the interaction between these two parts such that if there is a merge between a non-nominal and nominal node the tree-like structure should be maintained in order to take advantage of the blocking condition and avoid an infinite "generatingmerging" sequence, and (iii) we have to prevent a blocking node z from having a nominal descendant x with (≤ nS.C) ∈ L(x) (L(x) denotes a set of x's labels) such that the non-nominal predecessor y of x is an S-neighbor of x and C ∈ L(y). Such a node x may be "embarrassing" since this situation may lead to devise by "unraveling" a model that has a nominal individual (corresponding to x) connecting to an infinite number of distinct individuals (corresponding to y).

To obtain the conditions mentioned for termination, [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF] introduced some new rules which can add nominal nodes with new nominals and push "embarrassing" nodes into the non-tree part such that all merges related to such nodes are no longer required. It was shown that this process may add a double exponential number of new nominal nodes. This explains why the tableau-based algorithm presented in [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF] is not worst-case optimal.

Overview of the novel tableau-based algorithm

The observations from the previous section would make us think that adding new nominal nodes to obtain termination is not intrinsically related to the semantic constraints imposed by the logic constructors in SHOIQ. Rather, this behaviour results from the selected structure on which we know how to establish a mechanism to ensure termination. This structure requires to push "embarrassing" nodes into the non-tree part by generating new nominal neighbors, then merging one of them into a nonnominal neighbor. This implies that we could avoid adding new nominal nodes if the tree-like structure can be maintained by some way such that it allows us to avoid merging explicitly nominal nodes.

Although experiments indicate that the tableau and hypertableau-based algorithms for SHOIQ have good behaviours in practice, none of them was shown to be worstcase optimal. The contribution of the present paper consists in proposing a worst-case optimal tableau-based algorithm for checking consistency of a SHOIQ knowledge base. This algorithm is aimed at exploiting a structure which contains no non-tree part. As a result, we can reuse the usual blocking technique to ensure termination. The underlying idea of our approach is to introduce a function, namely partitioning function, which partitions the set of all nodes of tree-like structures. Roughly speaking, each partition represents a set of nodes that could be merged together. The expansion rules perform necessary propagations of labels between nodes and edges as if they are merged. More precisely, expansion rules related only to SHIQ constructors (i) perform local merges, i.e. the merges of a neighbor into another one are triggered by terms such as (≤ nS.C), (ii) propagate the node labels between nodes of a partition, and (iii) propagate the edge labels between edges that connect neighbor partitions. In turn, expansion rules related to nominals perform global merges, i.e. the merges of a neighbor partition into another one are triggered by merging nominal nodes or terms such as (≤ nS.C). The global merges update the partitioning function and do no change the tree-like structures except for labels.

Summing up, 1. For termination issue, our algorithm maintains tree-like structures which is built by applying the expansion rules related to SHIQ constructors. Thus, the standard blocking technique can be used to achieve termination. As a consequence, the size of tree-like structures is exponential in the size of input. 2. To avoid infinite sequences of "generating-merging", our algorithm does not perform explicitly merges triggered by nominal nodes. Instead, we employ a partitioning function over nodes for memorizing nodes that could be merged. 3. To help in devising correctly a model by unraveling over tree-like structures, we use a new rule, called -rule, which ensures that if there is a blocking node y that has a nominal descendant z then there exist two nodes w, w between y and z such that if w is a S-predecessor of w and L(w ) contains C then L(w) contains no term such as (≤ nS.C). In addition, this rule guarantees that if a leaf node z cannot be blocked by such a blocking node then there is a non-leaf node y such that z and y must belong to the same partition.

A Tableau for SHOIQ

Basically, a tableau structure is employed to represent a model of a SHOIQ knowledge base. Properties in a tableau definition for SHOIQ express the semantic constraints resulting directly from the logic constructors in SHOIQ. These properties show how a given individual of a tableau establishes relationships with other individuals in order to semantically satisfy each concept associated with the individual in question. As a result, these properties would guide us to design expansion rules that allow for building a finite representation of models.

Regarding the definition of tableaux for SHOIQ presented in [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF], we add a new property, namely P15. This new property imposes an exact number of S-neighbor individuals t of s if (≤ nS.C) ∈ L(s). This property makes explicit the nondeterminism implied from the semantics of (≤ nS.C) and requires an extra expansion rule, namely -rule, introduced in Algorithm 1. The presence of this rule may have an impact on the so-called "pay-as-you-go" behaviour of the tableau-based algorithm presented in this paper.

Definition 4 (tableau) Let (T , R) be a SHOIQ + knowledge base. A tableau T for (T , R) is defined to be a triplet (S, L, E) such that S is a non-empty set of individuals, L: S → 2 cl(T ,R) and E: R (T ,R) → 2 S×S . For all s ∈ S, C, C 1 , C 2 ∈ cl(T , R) and R, S ∈ R (T ,R) , T satisfies the following properties:

P1 If C 1 C 2 ∈ T then nnf(¬C 1 C 2 ) ∈ L(s), P2 If C ∈ L(s) then ¬C / ∈ L(s), P3 If C 1 C 2 ∈ L(s) then C 1 ∈ L(s) and C 2 ∈ L(s), P4 If C 1 C 2 ∈ L(s) then C 1 ∈ L(s) or C 2 ∈ L(s), P5 If ∀S.C ∈ L(s) and s, t ∈ E(S) then C ∈ L(t), P6 If ∀S.C ∈ L(s), Q * S, Trans(Q) and s, t ∈ E(Q) then ∀Q.C ∈ L(t), P7 If ∃P.C ∈ L(s) then there is t ∈ S such that s, t ∈ E(P ) and C ∈ L(t), P8 s, t ∈ E(R) iff t, s ∈ E(R ), P9 If s, t ∈ E(R) and R * S then s, t ∈ E(S), P10 If (≤ nS.C) ∈ L(s) then card{S T (s, C)} ≤ n, P11 If (≥ nS.C) ∈ L(s) then card{S T (s, C)} ≥ n where S T (s, C) := {t ∈ S| s, t ∈ E(S) ∧ C ∈ L(t)}, P12 If (≤ nS.C) ∈ L(s) and s, t ∈ E(S) then C ∈ L(t) or ¬C ∈ L(t) P13 If o ∈ L(s) ∩ L(t) for some o ∈ C o then s = t, P14 For each o ∈ C o , if o occurs in T then there is s ∈ S such that o ∈ L(s). P15 If (≤ nS.C) ∈ L(s)
and there is t ∈ S such that C ∈ L(t) and s, t ∈ E(S) then there is some 1 ≤ m ≤ n such that {(≤ mS.C), (≥ mS.C)} ⊆ L(s).

All properties of Definition 4 except for P15 are taken from [START_REF] Horrocks | Practical reasoning for expressive description logics[END_REF] and [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF]. If we say that an individual s has an R-neighbor t when s, t is an instance of R, then any application of properties to s imposes constraints only on s's neighbors or itself. This characteristic of tableaux will be called local property. The presence of role transitivity makes local property of tableaux more difficult to be ensured. (P6) in Definition 4 allows us to overcome this difficulty by avoiding representing all instances of transitive roles in a tableau. In order to satisfy a concept such as ∀S.C from an individual s where S is transitive, instead of propagating the concept C along with each instance of the transitive role S, it is sufficient to "push" C and the term ∀S.C to each S-neighbor t of s. As a consequence, the local property is guaranteed for SHIQ tableaux. However, it is much more difficult to preserve the local property of tableaux for logics which allow for transitive closure of roles. For instance, tableaux introduced in [START_REF] Duc | Decidability of SHI with transitive closure of roles[END_REF] for SHI with transitive closure of roles, namely SHI + , do not have the local property.

According to this argument, P13 in Definition 4 is responsible for the loss of local property in SHOIQ tableaux since P13 can be applied to two arbitrary individuals with which the same nominal is associated. The local property of tableaux has an important impact on the way by which a tableau-based algorithm can build completion graphs. For instance, each application of the expansion rules presented in [START_REF] Horrocks | Practical reasoning for expressive description logics[END_REF] for SHIQ performs some changes to its neighbours or itself. Then, checking clashfreeness can be performed on each node and its neighbors. On the contrary, the application of o-rule presented in [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF] for SHOIQ may change two arbitrary nodes while the algorithm introduced in [START_REF] Duc | Decidability of SHI with transitive closure of roles[END_REF] for concept satisfiability in SHI + has to check over the whole tree whether there exists a path for satisfying axioms such as R P + . As a consequence, the loss of local property may lead to augment the complexity, e.g., from EXPTIME-complete for SHIQ to NEXPTIME-complete for SHOIQ. The results from [START_REF] Tobies | Complexity results and practical algorithms for logics in knowledge representation[END_REF] have indicated that the concept satisfiability problems in ALC (with GCI) and SHIQ are EXPTIME-complete. This implies that the concept satisfiability problem in SHI is EXPTIME-complete due to ALC ⊆ SHI ⊆ SHIQ. It remains an open question whether the complexity of the satisfiability problem in SHI + is EXPTIME-complete.

Lemma 1 Let (T , R) be a SHOIQ knowledge base. (T , R) is consistent iff there is a tableau for (T , R).
A proof of a similar lemma for SHIQ tableaux can be found in [START_REF] Horrocks | A description logic with transitive and converse roles, role hierarchies and qualifying number restrictions[END_REF]. From this proof, it is not hard to prove Lemma 1 for SHOIQ tableaux with the new properties P13, P14 and P15.

A 2EXPSPACE decision procedure for SHOIQ

In this section, we introduce SHOIQ-trees with Definition 5. Intuitively, a SHOIQtree is defined by considering nominals as non-nominal concepts. The important difference between SHOIQ-trees and completion trees for SHIQ is the presence of a blocking condition with two layers that is governed by iterated and blocked nodes. An iterated node in a SHOIQ-tree whose root is a nominal node corresponds exactly to a blocked node in a completion tree for SHIQ. A blocked node y in a SHOIQ-tree is a descendant of an iterated node x such that the blocking condition for y is applied from x. That is x is considered as root of the subtree on which the condition blocking is applied to each blocked descendant y of x. The reason for introducing the blocking condition with two layers is to allow for defining inner nodes which will be presented in Definition 7.

Construction of the algorithm

Definition 5 (SHOIQ-tree) Let (T , R) be a SHOIQ knowledge base. For each o ∈ C o , a SHOIQ-tree for (T , R), denoted by T o = (V o , E o , L o , x o , • = o ), is de- fined as follows: * V o is a set of nodes containing a root node x o ∈ V o . Each node x ∈ V o is labelled with a function L o such that L o (x) ⊆ cl(T , R) and o ∈ L o ( x o ). A node x ∈ V o is called nominal if o ∈ L o (x) for some o ∈ C o .
In addition, the inequality relation

• = o is a symmetric binary relation over V o . * E o is a set of edges. Each edge x, y ∈ E o is labelled with a function L o such that L o ( x, y ) ⊆ R (T ,R) . * If x, y ∈ E o
then y is called a successor of x, denoted by y ∈ succ 1 (x), or x is called the predecessor of y, denoted by x = pred 1 (y). In this case, we say that x is a neighbour of y or y is a neighbour of x. If z ∈ succ n (x) (resp. z = pred n (x)) and y is a successor of z (resp. y is the predecessor of z) then y ∈ succ (n+1) (x) (resp. y = pred (n+1) (x)) for all n ≥ 0 where succ 0 (x) = {x} and pred 0

(x) = x. * A node y is called a descendant of x if y ∈ succ n (x) for some n > 0. A node y is called an ancestor of x if y = pred n (x) for some n > 0. To ensure that T o is a tree, it is required that (i) x is a descendant of x o for all x ∈ V o with x = x o , and (ii) each node x ∈ V o with x = x o has a unique predecessor. * A node y is called an R-successor of x, denoted by y ∈ succ 1 R (x) (resp. y is called the R-predecessor of x, denoted by y = pred 1 R (x)) if there is some role R such that R ∈ L o ( x, y ) (resp. R ∈ L o ( y, x )) and R * R. A node y is called a R-neighbour of x if y is either a R-successor or R-predecessor of x. If z is an R-successor of y (resp. z is the R-predecessor of y) and y ∈ succ n R (x) (resp. y = pred n R (x)) then z ∈ succ (n+1) R (x) (resp. z = pred (n+1) R (x)) for n ≥ 0 with succ 0 R (x) = {x} and x = pred 0 R (x)
. * For a node x, a role S and o ∈ C o , we define the set S To (x, C) of x's S-neighbors as follows:

S To (x, C) = {y ∈ V o | y is a S-neighbor of x and C ∈ L o (x)} * A node
x is called iterated by y w.r.t. a node x o if x has no nominal ancestor except for x o and there are integers n, m > 0 and nodes x , y such that

1. x o = pred n (y), y = pred m (x), 2. x = pred 1 (x), y = pred 1 (y), 3. L o (x) = L o (y), L o (x ) = L o (y ), 4. L o ( x , x ) = L o ( y , y ), and 5. if there are z, z and i > 0 such that z = pred 1 (z), pred i (z ) = x o , L o (z) = L o (y), L o (z ) = L o (y ) and L o ( z , z ) = L o ( y , y ) then i ≥ n. A node x is called 1-iterated by y if x is iterated by y w.r.t. x o . A node x is called blocked by y, denoted by y = b(x), if x is iterated by y w.r.t. a 1-iterated node x o . * In the following, we often use L(x), L( x, y ), S T (x, C) and • = instead of L o (x), L o ( x, y ), S To (x, C) and •
= o , respectively. This does not cause any confusion since

V o ∩ V o = ∅ and E o ∩ E o = ∅ if o = o . In addition, x • = o y is never defined for x ∈ V o and y ∈ V o with o = o .
We can remark that the definition of 1-iterated nodes in Definition 5 for SHOIQtrees is very similar to the standard definition of blocked nodes for SHIQ completion 1 SHOIQ-trees with a partitioning function ϕ illustrate the notions presented in Definition 5, 6 and 7. In this figure, two superimposed triangles represent 2 layers of a SHOIQ-tree. Nodes x, w are 1iterated while y 1 , y 2 , w 1 , w 2 are blocked nodes. Especially, z is a leaf node which is a nominal descendant of the blocking node y = b(y 2 ). In addition, we have

x w z To 1 To 2 w1 w2 y2 x x y y y1 w xo 1 w ϕ(z) xo 2 ϕ(z ) {o2, (≤ nR.C), (≥ nR.C)} ⊆ L(z) z Fig.
xo 2 ∈ ϕ(z) since o 2 ∈ L(z) ∩ L( xo 2 ). Due to {(≤ nR.C), (≥ nR.C)} ⊆ L(z), C ∈ L(z ), R ∈ L( z , z ) and L(z) = L( xo 2 ), there is a R-successor w of xo 2 such that w ∈ ϕ(z ) and C ∈ L(w ). According to Definition 7, z is inner.
trees (see [START_REF] Horrocks | Practical reasoning for expressive description logics[END_REF]). Moreover, if we consider the subtree rooted at a 1-iterated node as a SHIQ completion tree then blocked nodes according to Definition 5 are also blocked nodes according to the standard definition for this SHIQ completion tree.

In the sequel, following each definition we present some properties which are immediate consequences of the definition, and directly comment on them. When a property is not trivial, a proof can be found in the comment. Additionally, some notions or notations introduced in these properties would be used in proofs thereafter.

Property 1 Each leaf node of a SHOIQ-tree must be either a nominal or blocked node.

Comment: A nominal leaf node either is a descendant of a 1-iterated node or has no 1iterated ancestor. As we will show, each non-root nominal node can be grouped with a root node that is always nominal. This explains why we do not need to generate successors of a non-root nominal node. In Figure 1, z is a nominal leaf node while y 1 , y 2 , w 1 and w 2 are blocked nodes.

Property 2 A SHOIQ-tree consists of two layers : the first layer is formed of nodes from the root to 1-iterated nodes or nominal nodes, and the second layer consists of nodes from each 1-iterated node to blocked or nominal nodes. In addition, each node x in the layer 2 has a unique 1-iterated node, denoted b(x), such that b(x) is an ancestor of x.

Comment: In Figure 1, nodes x and x belong to the first layer and x is 1-iterated by x . Nevertheless, nodes y and y 1 belong to the second layer and y 2 is blocked by y.

Moreover, x = b(y 1 ) = b(y 2 ) = • • • and w = b(w 1 ) = b(w 2 ) = • • • .
The necessity of the two-layer structure of SHOIQ-trees will be clarified in properties and their comment following Definition 7.

Definition 6 (SHOIQ-forest) Let (T , R) be a SHOIQ knowledge base. A SHOIQ- forest for (T , R) is a pair G = T, ϕ , where T = {T o | o ∈ C o } is a set of SHOIQ-trees for (T , R) with T o = (V o , E o , L o , x o , • = o ), and ϕ is a partitioning function ϕ : V → 2 V with V = o∈Co V o . We denote L ( x, y ) = L o ( x, y ) if x, y ∈ E o , and L o ( x, y ) = {S | S ∈ L o ( y, x )} if y, x ∈ E o for some o ∈ C o .
The partitioning function ϕ satisfies the following conditions:

1. For each x ∈ V, ϕ(x) is the partition of x with x ∈ ϕ(x). There are x 0 , • • • , x n ∈ V such that ϕ(x i ) ∩ ϕ(x j ) = ∅ with 0 ≤ i < j ≤ n and 0≤i≤n ϕ(x i ) = V; 2. For all x, x ∈ V, if x ∈ ϕ(x) then ϕ(x) = ϕ(x ) and L(x) = L(x ). We denote Λ(ϕ(x)) = L(x).
In addition, an inequality relation over partitions can be described as follows : for x, x ∈ V we define ϕ(x) • =ϕ(x ) if there are two nodes y ∈ ϕ(x) and y ∈ ϕ(x ) such that y We define a function Λ( •, • ) for labelling edges ended by two partitions as follows:

Λ( ϕ(x), ϕ(x ) ) = L ( z, z ) where z ∈ ϕ(x), z ∈ ϕ(x ), L ( z, z ) = ∅, and { z, z , z , z } ∩ E o = ∅ for some o ∈ C o . We say ϕ(x ) is a S- neighbour partition of ϕ(x) if S ∈ Λ( ϕ(x), ϕ(x ) ). 4. For all x, x ∈ V, if o ∈ L(x) ∩ L(x ) for some o ∈ C o and ϕ(x) • =ϕ(x ) does not hold then ϕ(x) = ϕ(x ); and 5. If (≤ nR.C) ∈ Λ(ϕ(x)) for some x ∈ V and there exist n+1 nodes x 0 , • • • , x n ∈ V such that -ϕ(x i ) ∩ ϕ(x j ) = ∅ for all 0 ≤ i < j ≤ n, and -C ∈ Λ(ϕ(x i )), R ∈ Λ( ϕ(x), ϕ(x i ) ) for all i ∈ {0, • • • , n} then ϕ(x l ) • =ϕ(x m ) for all 0 ≤ l < m ≤ n. 6. If (≥ nR.C) ∈ Λ(ϕ(x)) for some x ∈ V then ϕ(x) has n R-neighbour partitions ϕ(x 1 ), • • • , ϕ(x n ) such that ϕ(x i ) ∩ ϕ(x j ) = ∅ and C ∈ Λ(ϕ(x i )) for all 1 ≤ i < j ≤ n.
* Clashes: T is said to contain a clash if one of the following conditions holds:

1. There is some node x ∈ V such that {A, ¬A} ⊆ Λ(ϕ(x)) for some concept name A ∈ C; 2. There are nodes x, y ∈ V such that ϕ(x) • =ϕ(y) and o ∈ Λ(ϕ(x)) ∩ Λ(ϕ(y)) for some o ∈ C o ; 3. There is a node x ∈ V with (≤ nR.C) ∈ Λ(ϕ(x)) and there are (n + 1) nodes

x 0 , • • • , x n ∈ V such that ϕ(x i ) ∩ ϕ(x j ) = ∅, ϕ(x i ) • =ϕ(x j ) with 0 ≤ i < j ≤ n, and C ∈ Λ(ϕ(x i )), R ∈ Λ( ϕ(x), ϕ(x i ) ) for i ∈ {0, • • • , n}.
The idea behind the notion of partitioning function is to capture the semantics of nominals and its consequences. Such a partitioning function determines a graph structure which is described by the following property:

Property 3 A SHOIQ-forest T, ϕ according to Definition 6 determines a graph G T ϕ = (V, E, Λ) where V is a set of nodes corresponding to partitions, i.e., V = {ϕ(x) | x ∈ V} and E is a set of edges with E = { ϕ(x), ϕ(y) | x , y ∈ E o , x ∈ ϕ(x), y ∈ ϕ(y), o ∈ C o }.
The nodes and edges of G T ϕ are labelled by Λ as described in Definition 6. It allows us to say that ϕ(y) is a neighbour of ϕ(x) if ϕ(x), ϕ(y) ∈ E or ϕ(y), ϕ(x) ∈ E, and that ϕ(y) is a R-neighbour of ϕ(x) if R ∈ Λ( ϕ(x), ϕ(y) ). In addition, there is an inequality relation

• = over V, i.e., ϕ(x) • =ϕ(y) iff there are x ∈ ϕ(x) and y ∈ ϕ(y) such that x • = o y for some o ∈ C o .
Comment: the conditions 1 and 2 in Definition 6 formulate the properties of an ordinary partitioning function while the conditions 3 and 4 show how to label nodes and edges of G T ϕ . More precisely, the condition 2 ensures that all nodes of a partition have the same label. Since the empty edge label is not needed to be propagated, the condition 3 guarantees that all non-empty edges ended by two nodes belonging to two given partitions have the same label. The conditions 4 and 5 take care of consequences resulting from the semantics of nominals. Indeed, if we consider nodes of G T ϕ as individuals of a tableau, and the inequality relation • = over V is respected, then the condition 4 ensures that for each o ∈ C o there is a unique partition ϕ(x) such that o ∈ Λ(ϕ(x)). Additionally, if (≤ nR.C) ∈ Λ(ϕ(x)) and the inequality relation • = over V is respected, then the condition 5 guarantees that node ϕ(x) has at most

n distinct R-neigbours ϕ(x 0 ), • • • , ϕ(x n-1 ) in G T ϕ such that C ∈ Λ(ϕ(x i )) for 0 ≤ i ≤ n -1. Note that ϕ(x) is different from ϕ(y), denoted ϕ(x) = ϕ(y), iff ϕ(x) ∩ ϕ(y) = ∅.
We now describe the tableau-based algorithm, namely Algorithm 3, whose goal is to construct from a knowledge base (T , R) a SHOIQ-forest G = T, ϕ . To do this, Algorithm 3 applies the expansion rules as described in Algorithm 1 and 2, and terminates when none of the rules is applicable. The obtained G is called complete, and if G contains no clash then G is called clash-free. In this case, we also say T o is complete and clash-free for all T o ∈ T. Before presenting these expansion rules, we introduce an operation, namely Propagate, which is used in expansion rules.

Propagation Propagate(ϕ(x), ϕ(x ), ϕ(y)) is an operation which propagates (i) node labels from a partition ϕ(x) to another partition ϕ(x ), and vice versa, (ii) edge labels from the edges ended by nodes of ϕ(x) and ϕ(y) to the edges ended by nodes of ϕ(x ) and ϕ(y), and vice versa. In other terms, Propagate(• • • ) merges ϕ(x) into ϕ(x ), and ϕ(x), ϕ(y) into ϕ(x ), ϕ(y) . More precisely, let G = T, ϕ be a SHOIQ-forest with

T = {T o | o ∈ C o } and T o = (V o , E o , L o , x o , • = o
). Propagate(ϕ(x), ϕ(x ), ϕ(y)) updates the label of nodes and edges in T as follows: x has no n S-neighbours y 1 , ..., yn such that C ∈ L(y i ), and y i • =y j for 1 ≤ i < j ≤ n, then create n new nodes y 1 , ..., yn with L( x, y i )={S}, L(y i )={C}, ϕ(y i ) = {y i } and y i

1. L(z) = L(x) ∪ L(x ) for all z ∈ ϕ(x) ∪ ϕ(x ), 2. for all z, z ∈ ϕ(x) ∪ ϕ(x ) and w, w ∈ ϕ(y), if z is a S-neighbour of w and L ( z , w ) = ∅ then (a) if z is a successor of w and S / ∈ L( w , z ) then L( w , z ) = L( w , z )∪ {S}, (b) if w is a successor of z and S / ∈ L( z , w ) then L( z , w ) = L( z , w )∪ {S }. -rule: if C D ∈ T and nnf(¬C D) / ∈ L(x) then L(x ) = L(x ) ∪ {nnf(¬C D)} for all x ∈ ϕ(x). -rule: if C 1 C 2 ∈ L(x) and {C 1 , C 2 } ⊆ L(x) then L(x ) = L(x ) ∪ {C 1 , C 2 } for all x ∈ ϕ(x). -rule: if C 1 C 2 ∈ (x) and {C 1 , C 2 } ∩ L(x) = ∅ then L(x ) = Lo(x ) ∪ {C} with some C ∈ {C 1 , C 2 } for all x ∈ ϕ(x). ∃-rule: if 1. ∃S.C ∈ L(x), x is not blocked, x
• =y j for 1 ≤ i < j ≤ n. ≤-rule: if 1. (≤ n S.C) ∈ L(x)
, and 2. card{S T (x, C)} > n and there are two S-neighbours y, z of x with C ∈ L(y) ∩ L(z), y is not an ancestor of z and not y

• =z then 1. for all z ∈ ϕ(z), x ∈ ϕ(x) such that L ( x , z ) = ∅, if x is an ancestor of z then L( x , z ) = L( x , z ) ∪ L( x, y ) else L( z , x ) = L( z , x ) ∪ {R | R ∈ L( x, y )} 2. L(z ) = L(z ) ∪ L(y) for all z ∈ ϕ(z) and L( x, y ) = ∅ 3. add u • =z for all u such that u • =y. -rule: if 1. (≤ nR.C) ∈ L(x), {(≤ l R.C), (≥ l R.C)} L(x) for all l ≤ n, 2. (≤ k R.C) / ∈ L(x)
for all k < n, and 3.

x has a R-neighbour y such that C ∈ L(y) then 1. guess m with 1 ≤ m ≤ n, and 2. L(x ) = L(x ) ∪ {≤ mR.C, ≥ mR.C} for all x ∈ ϕ(x).

Figure 1: Expansion rules for SHIQ

In the following, we discuss and stress new aspects of the expansion rules in Algorithm 1 and 2 for SHOIQ.

The rules in Algorithm 1 maintain the tree-like structure of SHOIQ-forest and they are similar to those in [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF] except that if a concept C is added to the label of a node x due to application of these rules then C is propagated to the label of each node y ∈ ϕ(x). Moreover, all rules in Algorithm 1 except for ∃and ≥-rule update only the label of nodes or edges and do no change on the partitioning function ϕ. Especially, when the ≤-rule is applied to a node x with two S-neighbours y, z of x, it must propagate the label of x, y to that of all x , z (or z , x ) where x ∈ ϕ(x) and z ∈ ϕ(z), and set the label of x, y to empty set. This may change ϕ only if ϕ(y) is singleton.

A new feature of the generating rules (∃-rule and ≥-rule) with respect to those in [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF] is that these rules are not applied to non-root nominal nodes. By Definition 6, a non-root nominal node belongs always to the partition ϕ( x o ) where x o is a root node (note that all root nodes are nominal). As a result, it is not necessary to generate successors of a non-root nominal node since it "inherits" all neighbours of x o .

oϕ-rule: We would like to stress the difference between the ≤-rule in Algorithm 1 and the ≤ ϕ -rule in Algorithm 2. Basically, the ≤-rule with the others in Algorithm 1 ensures that the semantic constraints (except for nominals) imposed by the label of each node are satisfied. The rule ≤ ϕ -rule with o ϕ -rule takes care of the semantic constraint of nominals and its consequences, i.e., these rules deal with partitions rather than nodes, and do no change on the structure of trees. The necessity of both rules is a consequence of the two-part structure for models of a SHOIQ knowledge base : (i) the first part which is finite and contains nominals, will be constructed from partitions, (ii) the second part will be built by unravelling subtrees which contain no nominals and are maintained by SHIQ-rules. Note that the ≤-rule and ≤ ϕ -rule are complementary, i.e., when one of these rules has been applied to a node the other one may be applicable to the same node. For instance, after applying the ≤ ϕ -rule to a node x with (≤ nS.C) ∈ L(x), x may have (n + 1) S-neighbours containing C since a S-neighbour partition of ϕ(x) may contain two S-neighbours that include C. Another aspect that needs to be clarified is that when two partitions ϕ(y ) and ϕ(y ) combine to obtain the new partition ϕ(y ) ∪ ϕ(y ), the inequality relations are automatically transfered from ϕ(y ) and ϕ(y ) to ϕ(y ) ∪ ϕ(y ) due to the definition of inequality relation over partitions. Indeed, if there is some ϕ(z) such that ϕ(z) • =ϕ(y ) (resp. ϕ(z) • =ϕ(y )), i.e., there are some z ∈ ϕ(z) and w ∈ ϕ(y

if 1. there are nodes x, x with o ∈ L(x) ∩ L(x ) for some o ∈ Co, 2. ϕ(x) ∩ ϕ(x ) = ∅ and ϕ(x) • =ϕ(x ) does not hold, then 1. Propagate(ϕ(x), ϕ(x ), ϕ(y)) for each y such that { x , y , y, x } ∩ Eo = ∅ for x ∈ ϕ(x) ∪ ϕ(x ), o ∈ Co. 2. ϕ(y ) = ϕ(x) ∪ ϕ(x ) for all y ∈ ϕ(x) ∪ ϕ(x ). ≤ϕ-rule: if 1. (≤ nR.C) ∈ L(x), 2. there are nodes y 0 , • • • , yn with ϕ(y i ) ∩ ϕ(y j ) = ∅, 0 ≤ i < j ≤ n, C ∈ Λ(ϕ(y i )), R ∈ Λ( ϕ(x), ϕ(y i ) ) for all 0 ≤ i ≤ n,
) (resp. w ∈ ϕ(y )) with z • = o w and o ∈ C o then ϕ(z) • =ϕ(y ) ∪ ϕ(y ) since w ∈ ϕ(y ) ∪ ϕ(y ).
By the -rule, each node x containing a term (≤ nS.C) has exactly m Sneighbours containing C with some m ≤ n. As a result, this rule and ≥-rule ensure that if there are two nodes y, y ∈ ϕ(x) then y and y have exactly m S-neighbours which contain C in their label.

Finally, we can avoid infinite sequences of "merging-and-generating", the socalled "yo-yo" effect ( [2], [3]), in the tableau algorithm presented in this paper without pruning nodes, since all merges due to number restrictions or nominals are performed by updating the partitioning function. We will clarify how it works by examples in Section 5.2.

In the sequel, we present the specific features of a complete and clash-free SHOIQforest. These features, which are related to the notions introduced in Definition 7, are crucial to establish soundness of the tableau algorithm presented in this paper. Basically, the goal of the soundness proof is to build a tableau from a complete and clash-free SHOIQ-forest. For this purpose, we use the technique introduced in [START_REF] Horrocks | Practical reasoning for expressive description logics[END_REF] to define paths (corresponding to individuals of the tableau) which are originated from the root node of each T o ∈ T, go down through successors of a node and may be infinitely lengthened by "unraveling". The specific features of complete and clash-free SHOIQ-trees make such paths avoid infinitely going through nominal nodes.

T o = (V o , E o , L o , x o , • = o ). * Core node: A node x ∈ V o with o ∈ C o is called core node if x has a nominal descendant z with x = pred k (z) (k ≥ 0) such that there are (≤ n i R i .C i ) ∈ L(pred i (z)), R i ∈ L( pred (i+1) (z), pred i (z) ), C i ∈ L(pred i+1 (z)) for 0 ≤ i ≤ (k -1). * Inner node: A node x ∈ V o with o ∈ C o is called inner node if 1.
x is a descendant of a 1-iterated node; and 2. x is a core node. * Unravellable node: A node x ∈ V o with o ∈ C o is called unravellable node if the following conditions are satisfied:

1. x is blocked; 2. b(x) is not a core node; and 3. if b(x) has a blocked descendant y such that b(y ) = pred m (b(x)) (m > 0) then b(y ) is not a core node.
Before providing the intuition behind the notions introduced in Definition 7, we formulate and prove an immediate consequence of the definition of inner node.

Property 4 If a node x ∈ V o is inner for some o ∈ T o then there is an ancestor x of a 1-iterated node such that ϕ(x) = ϕ(x ).

Comment: By definition, there is a nominal node z with x = pred k (z) (k ≥ 0). Since T o is complete, i.e. -rule and o-rule are not applicable, we have

o ∈ L( x o ), ϕ(z) = ϕ( x o ), and thus {(≤ n 0 R 0 .C 0 ), (≥ n 0 R 0 .C 0 )} ⊆ L( x o ). Due to non- applicability of N N -, ≥-and ≤ ϕ -rules, it holds that x o has a R 0 -successor w 1 such that ϕ(pred 1 (z)) = ϕ(w 1 ), and thus {(≤ n 1 R 1 .C 1 ), (≥ n 1 R 1 .C 1 )} ⊆ L(w 1 ). This implies that w 1 has exactly n 1 distinct R 1 -neighbours u 1 , • • • , u n1 with C 1 ∈ L(u i ). Since z = pred 2 (z) it holds that w 1 has a R 1 -successor w 2 such that ϕ(pred 2 (z)) = ϕ(w 2 ), and thus {(≤ n 2 R 2 .C 2 ), (≥ n 2 R 2 .C 2 )} ⊆ L(w 2 )
. By the same argument, there are w i = succ i ( x To ) such that ϕ(pred i (z)) = ϕ(succ i ( x o )) for all 0 ≤ i ≤ k. Moreover, succ k ( x o ) must belong to the layer 1 of T o since the path from pred k (z) to z contains no two identical edges which are necessary to bring succ k ( x o ) to the layer 2.

The rule -rule is crucial to establish Property 4. This rule makes paths from a nominal node to its inner ancestors "hard", i.e., nodes of such paths cannot be duplicated by unravelling.

Intuition behind the notion of inner node. A node x belonging to the layer 1 of a complete SHOIQ-tree T o ∈ T is completely expanded by the rules in Algorithm 1 and 2, i.e., all neighbours of x and thus all neighbour partitions of ϕ(x) are generated. Moreover, if a node y is located in the layer 2 of T o and y is inner, i.e., ϕ(y) = ϕ(x) for some x located in the layer 1 (by Property 4), then y can be considered as completely expanded since all neighbour partitions of ϕ(y) are determined from x. It allows us to omit the subtree rooted at y, denoted by T o [y], when constructing a tableau in the soundness proof of Algorithm 3. Notice that the two-layer structure of SHOIQ-trees helps avoid "breaking" the inner nodes which "refer" to nodes in T o [y] after omitting T o [y]. Indeed, it is possible to omit the subtree T o [y] rooted at an inner node y only if (i) there is a node x such that x is completely expanded with y ∈ ϕ(x), and (ii) there is no inner node y such that ϕ(y ) = {y } ∪ X where X are a subset of nodes of T o [y]. It is obvious that we cannot obtain this property if we adopt the one-layer structure (which includes nodes from root to 1-iterated nodes) for SHOIQ-trees.

Intuition behind the notion of unravellable node. A blocked node x is called unravellable according to Definition 7 if we can infinitely lenghthen without violating number restrictions the paths (considered as tableau individuals) which go through the predecessor of x, then b(x) and so on. To attain this goal, Definition 7 requires that (i) if there is a nominal node z between b(x) and a blocked descendant y of b(x) then there exists a non-inner node y z between b(x) and z, and (ii) otherwise, i.e., if there is no nominal node between b(x) and a blocked descendant y of b(x) then y must be unravellable.

It is obvious that if this requirement is met we can infinitely duplicate the edges ended by the nodes from b(x) to nodes y z or to unravellable nodes y. As a result, infinite paths can be formed from these duplicated edges without violating number restrictions.

Property 5 If a blocked node x has no inner ancestor then x is unravellable.

Comment: Assume that x is not unravellable. According to the definition of unravellable nodes, there are the two following possibilities: In the following section, we present different examples to illustrate the main features of Algorithm 3 and discuss on how the algorithm deals with the main issues such as "yo-yo" effect and exponential blow-up of new nominals, etc. The section starts by running the algorithm with a simple knowledge base. The goal is to show how a partitioning function can help to avoid merging. Next, we will execute the algorithm with some interesting knowledge bases taken from [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF] and [START_REF] Motik | Hypertableau reasoning for description logics[END_REF].

Examples of applying the algorithm

An example of getting started.

We consider a knowledge base K 1 consisting of the following axioms: 2 A SHOIQ-tree with a partitioning function ϕ for the example According to Algorithm 3, there is only one SHOIQ-tree T = (V, E, L, x o , • =) which will be built since there is one nominal o in the knowledge base. In the same way, we can continue applying ∃-rule, ∀-rule, ∀ + , -rule and -rule to yield x 2 , x 3 , x 4 , x 5 and y 1 , y 2 , y 3 , y 4 such that x 2 , y 1 are successors of x 1 ; x 3 , y 2 are successors of x 2 ; x 4 , y 3 are successors of x 3 , and x 5 , y 4 are successors of x 4 . In addition, L(y

R 1 = {F R, Trans(R)}, T 1 = { ∃S.o, o ¬C ∃F.C ∀R.∃F.C} 0 1 x 3 x 5 x 2 x 1 xo ϕ( xo) y 0 y 1 y 2 y 3 y 4 x 4 {R, F } {S} {S} {S} {S} {S} {R, F } {R, F } {R, F } {R, F } Fig.
i ) = L( x o ) for i ∈ {1, • • • , 4} and L(x j ) = L(x 1 ), ϕ(x j ) = {x j } for j ∈ {2, • • • , 5}.
At this stage, o ϕ -rule can be applied to nominal nodes From the definition of 1-iterated and blocked nodes, we obtain that x 3 is 1-iterated by x 2 and x 5 is blocked by x 4 . In addition, y i for i ∈ {0, • • • , 4} are nominal leaves. It is obvious that the obtained T is complete and clash-free. Therefore, K 1 is consistent.

We now modify slightly K 1 to obtain K 1 as follows.

R 1 = {F R, Trans(R)}, T 1 = { ∃S.(o (≤ 1S -. )), o ¬C ∃F.C ∀R.∃F.C}
When the at-most number restriction (≤ 1S -. ) occurs in the axiom, -rule is applicable to y i for i ∈ {1, • • • , 4} since (≤ 1S -. ) ∈ L(y i ). This rule guesses a unique m = 1 and adds (≤ 1S -. ), (≥ 1S -. ) to L(y i ). In turn, application of o ϕ -rule and ≤ ϕ -rule must group all nodes to a unique partition ϕ( x o ). This implies that {C, ¬C} ⊆ Λ(ϕ( x o )). Thus, K 1 is not consistent.

An example of dealing with the "generate-and-merge" problem.

This problem, known as "yo-yo" effect for DLs with nominals, is discused in [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF] and [START_REF] Motik | Hypertableau reasoning for description logics[END_REF]. These works proposed pruning nodes to prevent an infinite sequence of "generating-and-merging". Since Algorithm 3 performs no merge, such infinite sequences of "generating-and-merging" can be avoided by lengthening branches of a SHOIQ tree until blocked nodes occur.

To clarify this, we consider the following KB which is taken from [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF]:

K 2 = {A ∃R.(A ∃R.(A ∀R -.o)), o A} First, a root node x o is created with L( x o ) = {o} and ϕ( x o ) = { x o }.
Then, by applying -, ∃-, -rule to x o , we create a R-successor x 1 of x o , and a R-successor

x 2 of x 1 with ϕ( x o ) = { x o }, ϕ(x 1 ) = {x 1 }, ϕ(x 2 ) = {x 2 } and : L( x o ) ⊇ {o, A, ∃R.(A ∃R.(A ∀R -.o))}, L(x 1 ) ⊇ {A, ∃R.(A ∀R -.o)} L(x 2 ) ⊇ {A, ∀R -.o, A ∀R -.o}
Then, application of ∀-rule to x 2 adds o to L(x 1 ), which leads to apply o-rule to x 1 and x o . We now obtain the following partitions :

ϕ( x o ) = { x o , x 1 } and ϕ(x 2 ) = {x 2 } with L( x o ) = L(x 1 ) ⊇ {o, A, ∃R.(A ∀R -.o), ∃R.(A ∃R.(A ∀R -.o))}, L(x 2 ) ⊇ {A, ∀R -.o, A ∀R -.o}
We continue applying -rule and ∃-rule to x 2 in order to create a R-successor x 3 of x 2 , then apply ∃-rule to x 3 in order to create a R-successor x 4 of x 3 . At this stage, x 4 is blocked by x 2 since L(x 4 ) = L(x 2 ) and L( x 0 ) = L(x 1 ) = L(x 3 ) with ϕ( x o ) = { x o , x 1 , x 3 }. Therefore, the algorithm could avoid "yo-yo" effect without pruning nodes.

Note that the algorithm will create another R-successor x 1 of x 0 with L(x 1 ) = L(x 2 ) since the term ∃R.(A ∀R -.o) is propagated from x 1 to x 0 .

Soundness and completeness of the algorithm

As mentioned in Section 5.1, we establish soundness of the algorithm by construcing a tableau from a complete and clash-free set of SHOIQ-trees with a partitioning function. The proof given in this section is founded on the notions introduced in Definition 7 and Properties 5 and 4.

Lemma 2 (Termination) Let (T , R) be a SHOIQ knowledge base. Algorithm 3 terminates and builds SHOIQ-trees whose the size is bounded by a double exponential function in the size of (T , R).

Proof First, we compute a upper bound of the SHOIQ tree's depth from the blocking condition. This upper bound equals K = 2 2m+k ×2 where m = card{cl(T , R) }, and k is the number of roles occurring in T and R plus their inverse. Moreover, the number of neighbours of any node is bounded by M = m i where M = m i +E, m i occurs in a number restriction term (≥ m i R.C) appearing in T and E is the number of distinct terms ∃R.C appearing in T . This implies that the size of SHOIQtrees is bounded by M 2 2m+k ×2 .

Applications of rules in Algorithm 1 and 2 neither remove concepts from the label of nodes, nor remove roles from the label of edges except for setting the label of some edges to empty. However, when the label of an edge is set to empty it remains to be empty forever. Moreover, no rule attempts to remove nodes and edges from trees. Regarding to the partitioning function ϕ, it does no change on the structure of trees. Furthermore, partitions are never shrunken following application of the rules.

We have shown that (i) the size of SHOIQ-trees is bounded, (ii) the number of nodes and edges never decreases, (iii) the label of nodes and edges are never reduced, (iv) partitions are never reduced, and (v) each application of the rules either creates a node, or changes node, edge labels or partitions. Therefore, termination of the algorithm is a consequence of these facts.

Lemma 3 (Soundness) Let (T , R) be a SHOIQ knowledge base. If Algorithm 3 answers "YES" by yielding a clash-free and complete set of SHOIQ-trees for (T , R) then there is a tableau for (T , R).

Proof Assume that T = {T o | o ∈ C o }
is a set of clash-free SHOIQ-trees with a function ϕ which is built by Algorithm 3 for (T , R) where

T o = (V o , E o , L, x o , • = o ).
First, we show that ϕ satisfies all conditions of a partitioning function as described in Definition 6.

-The condition 1 is satisfied since the generating rules (∃-rule and ≥-rule) always define ϕ(x) for each fresh node x. In addition, the set ϕ(x) is never shrunken by applying expansion rules for all x. Moreover, all expansion rules either define ϕ(x) for a fresh node x or combine ϕ(x) with ϕ(y) to redefine ϕ(y ) = ϕ(x) ∪ ϕ(y) for all y ∈ ϕ(x) ∪ ϕ(y). -The condition 2 holds since (i) the condition 1 implies that if x ∈ ϕ(x) then ϕ(x ) = ϕ(x), (ii) when the generating rules are applied to a node x, fresh nodes y i are created with ϕ(y i ) = {y i }, (ii) when the other rules are applied to a node x, this may change the label of x and propagate (due to the operation Propagate if ϕ o -rule, and ≤ ϕ -rule are applied) added concepts to the label of all nodes of the partition containing x, i.e., ϕ(x). -The condition 3. If ϕ(x) and ϕ(x ) are singleton then the condition 3 is obvious.

Assume that ϕ(x ) (or ϕ(x)) is not singleton. This implies that ϕ(x ) is formed by an application of o ϕ -rule or ≤-rule. In this case, the condition 3 holds due to the definition of the operation Propagate. -The condition 4. Assume that o ∈ L(x) ∩ L(x ) and x • =x does not hold. Since T is clash-free, ϕ(x) • =ϕ(x ) does not hold. Moreover, since T is complete the o ϕrule is not applicable. This implies that ϕ(x) ∩ ϕ(x ) = ∅. Due to the condition 2, we have ϕ(x) = ϕ(x ).

-The condition 5 holds due to ≤ ϕ -rule.

-The condition 6 holds due to ≥-rule. In fact, we never merge two neighbour partitions ϕ(x i ) and ϕ(x j ) such that ϕ(x i ) • =ϕ(x j ).

Before constructing a tableau from T = {T o | o ∈ C o }, we introduce some notions and properties that are used in this construction.

Let I be the set of all inner nodes x such that x has no inner ancestor. Let B be the set of all blocked nodes y such that y has no ancestor that belongs to I. This implies that each y ∈ B is unravellable due to Property 5.

We use B to denote the set of nodes x ∈ B such that each x ∈ ϕ(x) is not an ancestor of a node y ∈ B ∪ I. As a consequence, if x ∈ B \ B then x does not need to be unravelled.

For y ∈ B, if b(y) has an inner descendant z with b(y) = pred k (z) then there is a node w = pred i (z) with 0 < i ≤ k such that w is not inner (otherwise, y is not unravellable). Let l be the least number such that w z = pred l (z) is not inner and w z has no inner ancestor. We use Ī to denote the set of successors of all w z . This implies that Ī ⊆ I.

For

-We use V ϕ(x) o to denote the set of T ϕ(x) o 's nodes. For each node v ∈ V ϕ(x) o , the set of v's successors in T ϕ(x) o is denoted by succ 1 (v). We initialize V ϕ(x) o = {b 1 (ϕ(x))} and p(b 1 (ϕ(x))) = b(x) where b 1 (ϕ(x)) is the root of T ϕ(x) o . -For each x ∈ succ 1 (p(v)) with v ∈ V ϕ(x) o , -If x is not blocked and x / ∈ Ī then we add to V x o and succ 1 (v) a new node v that is a successor of v with L( v, v ) = L( p(v),
x ), and define p(v ) =

x . -If x is unravellable (note that each blocked descendant y of b(x) such that y has no inner ancestor, is unravellable) then we add to

V ϕ(x) o and succ 1 (v) a new node v with L( v, v ) = L( p(v), x ), and define p(v ) = b(x ).
Note that all nodes of T ϕ(x) o

are duplicated from the non-inner nodes of the subtrees rooted at b(x) or b(x ) where b(x ) is an ancestor of b(x). We now define a tableau T = (S, L , E) as follows:

-S = S 1 ∪ S 2 where -S 1 = {ϕ(x) | x = pred i (x ), x ∈ I ∪ B, i ≥ 1}, and L (ϕ(x)) = Λ(ϕ(x)) -S 2 = x∈ B∩Vo, o∈Co V ϕ(x) o
, and

L (v) = L(p(v)) for v ∈ V ϕ(x) o -E(R) = E 1 (R) ∪ E 2 (R) ∪ E 3 (R) ∪ E 4 (R) where E 1 (R) = { ϕ(x), ϕ(y) ∈ S 1 × S 1 | R ∈ Λ( ϕ(x), ϕ(y) )} , E 2 (R) = { s, t ∈ S 2 × S 2 | R ∈ L( p(s), p(t) ) ∨ R ∈ L( p(t), p(s) )} E 3 (R) = { ϕ(x ), b 1 (ϕ(x)) ∈ S 1 × S 2 | R ∈ Λ( ϕ(x ), ϕ(x) )} ∪ { b 1 (ϕ(x)), ϕ(x ) ∈ S 2 × S 1 | R ∈ Λ( ϕ(x ), ϕ(x) )} E 4 (R) = { s, ϕ(w) ∈ S 2 × S 1 | R ∈ L( p(s), w ), w ∈ Ī} ∪ { ϕ(w), s ∈ S 1 × S 2 | R ∈ L( p(s), w ), w ∈ Ī}.
From the definition of the tableau T , we remark that S 1 is finite and contains nominals while S 2 is infinite. Moreover, ϕ(x) may belong to S 1 even if x ∈ I ∪ B since x may have an ancestor x which is an ancestor of a node y ∈ I ∪ B. Regarding role instances, E 3 (R) includes role instances from the predecesor of an unravellable node x to a copy of b(x). E 4 (R) contains an infinite number of role instances from non-inner nodes to inner nodes.

We now show that T satisfies all properties in Definition 4.

-P1-P4 hold due to the non-applicability of -rule, -rule and -rule in Algorithm 1 and the facts that T is clash-free. -For P5, assume that s, t ∈ S and ∀S.C ∈ L (s). By the definition of T , we consider the following cases:

s, t ∈ E 1 (S). This implies that there are x, y such that s = ϕ(x), t = ϕ(y) and ∀S.C ∈ Λ(ϕ(x)), Q ∈ Λ( ϕ(x), ϕ(y) ). By the definition of Λ( ., . ), there are x ∈ ϕ(x) and y ∈ ϕ(y) such that Q ∈ L ( x, y ) (note that L ( ., . ) is defined for edges of T in Definition 6). Due to the non-applicability of ∀-rule, it follows that C ∈ L(y ). By the definition of T and T, we have

C ∈ L (t). -s, t ∈ E 2 (S). This implies that ∀S.C ∈ L(p(s)), Q ∈ L ( p(s), p(t) ).
Due to the non-applicability of ∀-rule, it follows that C ∈ L(p(t)). By the definition of T , we have C ∈ L (t). s, t ∈ E 3 (S). This implies that there are x, y such that (i

) either s = ϕ(x), t = b 1 (ϕ(y)) ∈ V ϕ(y) o
with some o ∈ C o and ∀S.C ∈ L(x ), Q ∈ L ( x , y ) with x ∈ ϕ(x) and y ∈ ϕ(y). Due to the non-applicability of ∀-rule, C ∈ L(y ), or (ii) t = ϕ(x), s = b 1 (ϕ(y)) with ∀S.C ∈ L(y ), Q ∈ L ( y , x ), x ∈ ϕ(x) and y ∈ ϕ(y). Due to the non-applicability of ∀-rule, it follows that C ∈ L(x ). By the definition of T , we have C ∈ L (t).

s, t ∈ E 4 (S). This implies that either (i) S ∈ L( p(s), w ) with ∀S.C ∈ L(p(s)) and t = ϕ(w) for some w ∈ Ī. Due to the non-applicability of ∀rule, C ∈ L(w), or (ii) S ∈ L( p(t), w ) with ∀S.C ∈ L(w), s = ϕ(w).

Due to the non-applicability of ∀-rule, C ∈ L(p(t)). By the definition of T , we have C ∈ L (t). -P6. Analogously. -P7. Assume that s ∈ S 1 and ∃S.C ∈ L (s). Let s = ϕ(x) with ∃S.C ∈ L(x).

This implies that there is a node x ∈ I ∪ B such that x = pred i (x ) with i ≥ 1.

That means that x is not a leaf node. Due to the non-applicability of ∃-rule, x has a S-neighbour y with C ∈ L(y). We consider the following cases:

y ∈ I or y ∈ B \ B. By definition, there is some node y ∈ ϕ(y) such that y is an ancestor of a node z ∈ I ∪ B. This implies that ϕ(y) ∈ S 1 with C ∈ L (ϕ(y)), and ϕ(x), ϕ(y

) ∈ E 1 (R). -y ∈ B. We have b 1 (ϕ(y)) ∈ S 2 with C ∈ L (b 1 (ϕ(y))), and ϕ(x), b 1 (ϕ(y)) ∈ E 3 (R). -Otherwise, i.e., y / ∈ I ∪ B.
By definition, we have ϕ(y) ∈ S 1 with C ∈ L (ϕ(y)), and ϕ(x), ϕ(y) ∈ E 1 (R).

Assume that s ∈ S 2 with s ∈ V , s has a S-neighbour

v ∈ V ϕ(x) o such that C ∈ L(v ). If y is the predecessor of b(y) then C ∈ Λ(ϕ(x)) and s, ϕ(x) ∈ E 4 (S). -Otherwise, due to the definition of V ϕ(x) o , s has a S-neighbour v ∈ V ϕ(x) o such that C ∈ L(v ).
-P8 and P9 holds due to the construction of T .

-For P10, assume that s ∈ S with (≤ nS.C) ∈ L (s). We consider the following cases:

• Assume s ∈ S 1 i.e. s = ϕ(x) such that x = pred i (x ), i ≥ 1 for some x ∈ I ∪ B. Assume that there are distinct s 0 , • • • , s n ∈ S such that C ∈ L (s i ) and s, s i ∈ E(S) for 0 ≤ i ≤ n. Assume that s 0 , • • • , s n ∈ S 1 .
This implies that there are nodes

x 0 , • • • , x n such that ϕ(x i ) ∩ ϕ(x j ) = ∅, S ∈ Λ(ϕ(x), ϕ(x i )) and C ∈ Λ(ϕ(x i )) for 0 ≤ i < j ≤ n.
Due to the non-applicability of ≤-rule, there do not exist y , y such that ϕ(y

) ∩ ϕ(y ) = ∅, not ϕ(y ) • =ϕ(y ), S ∈ Λ(ϕ(x), ϕ(y )), S ∈ Λ(ϕ(x), ϕ(y )) and C ∈ Λ(ϕ(y ))∩Λ(ϕ(y )). This implies ϕ(x i ) • =ϕ(x j ) for all 0 ≤ i < j ≤ n, which contradicts clash-freeness of T. Assume that s 0 , • • • , s l ∈ S 2 and s l+1 , • • • , s n ∈ S 1 with 0 ≤ l < n. Due to the definition of S 1 there are nodes w l+1 , • • • , w n such that ϕ(w i ) ∩ ϕ(w j ) = ∅, C ∈ Λ(ϕ(w i )) and S ∈ Λ( ϕ(x), ϕ(w i ) ) for (l + 1) ≤ i < j ≤ n. Assume that s 0 ∈ V ϕ(y) o
and ϕ(x), s 0 ∈ E 4 (S). By the definition of T , this means that p(s 0 ) is a S -predecessor of a node w ∈ Ī with w ∈ ϕ(x). According to Property 4 (with (≤ nS.C) ∈ L(w), C ∈ L(p(s 0 ))), p(s 0 ) is inner since p(s 0 ) belongs to the layer 2. It contradicts the definition of Ī which contains no node whose predecessor is inner. We have shown that if s i ∈ S 2 then it is not possible that ϕ(x), s i ∈ E 4 (S) for all 0 ≤ i ≤ l. This implies that ϕ(x), s i ∈ E 3 (S) for all 0 ≤ i ≤ l. According to the definition of T , there nodes

w 0 , • • • , w l ∈ B such that ϕ(w i ) ∩ ϕ(w j ) = ∅, C ∈ Λ(ϕ(w i )) and S ∈ Λ( ϕ(x), ϕ(w i ) ) for 0 ≤ i < j ≤ l.
Due to the definition of B, we have ϕ(w i ) / ∈ S 1 for all 0 ≤ i ≤ l. Since S 1 ∩ S 2 = ∅, we have ϕ(w i ) ∩ ϕ(w j ) = ∅ for all 0 ≤ i < j ≤ n, which contradicts clash-freeness of T.

• Assume s ∈ S 2 , i.e., s ∈ V ϕ(x) o for some x ∈ B. Assume that there are distinct s 0 , • • • , s n ∈ S such that C ∈ L (s i ) and s, s i ∈ E(S) for 0 ≤ i ≤ n. Due to the non-applicability of ≤-rule, p(s) has at most n S-neighbours x 1 , • • • , x n with C ∈ L(x i ). Due to the definition of T , there are at most n individuals

s 1 , • • • , s n such that s, s i ∈ E(S) and C ∈ L (s i ). -To show P11, assume that s ∈ S 1 with (≥ nR.C) ∈ L (s) i.e. s = ϕ(x) with x = pred i (x ), i ≥ 1 for some x ∈ I ∪ B. Due to the non-applicability of ≥-rule, x has n S-neighbours x 1 , • • • , x n such that x i • =x j with C ∈ L(x i ) for 1 ≤ i < j ≤ n. This implies ϕ(x i ) ∩ ϕ(x j ) = ∅ and for all 1 ≤ i < j ≤ n. Moreover, if x i ∈ I, x i ∈ B \ B or x i = pred k (x ), k ≥ 1 for some x ∈ I ∪ B then ϕ(x i ) ∈ S 1 , ϕ(x), ϕ(x i ) ∈ E(S) and C ∈ L (ϕ(x i )). Other- wise, i.e., if x i ∈ B, then b 1 (ϕ(x i )) ∈ S 2 , ϕ(x), b 1 (ϕ(x i )) ∈ E(S) and C ∈ L (b 1 (ϕ(x i )). Due to b 1 (ϕ(x i )) = b 1 (ϕ(x j )) if ϕ(x i ) ∩ ϕ(x j ) = ∅ and S 1 ∩ S 2 = ∅, s has n distinct individuals s 1 , • • • , s n correponding to ϕ(x 1 ), • • • , ϕ(x n ) such that s, s i ∈ E(S) and C ∈ L (s i ). Assume that s ∈ S 2 with (≥ nR.C) ∈ L (s) , i.e., s ∈ V ϕ(x) o for some x ∈ B. Due to the non-applicability of ≥-rule, x has n S-neighbours x 1 , • • • , x n such that x i • =x j with C ∈ L(x i ) for 1 ≤ i < j ≤ n. This implies ϕ(x i ) ∩ ϕ(x j ) = ∅
and for all 1 ≤ i < j ≤ n. (we have to distinguish two rules for at most).

-For P12 assume that s, t ∈ S with (≤ nS.C) ∈ L (s) and s, t ∈ E(S). Assume s ∈ S 2 , i.e., s ∈ V ϕ(x) o

for some x ∈ B. If s = b 1 (ϕ(x)) and t = ϕ(y) with ϕ(y) ∈ S 1 then b(x) has a S-predecessor y with L(y ) = L(y). Due to the non-applicability of ch-rule, C ∈ L(y ). This implies that C ∈ L (t).

If s = b 1 (ϕ(x)) and t ∈ S 2 then p(t) is a S-neighbour of p(s). Due to the non-applicability of ch-rule, C ∈ L(p(t)) = L (t). If s = b 1 (ϕ(x)
) and t ∈ S 1 with t = ϕ(y) and y ∈ Ī then y is a S-neighbour of p(s). Due to the non-applicability of ch-rule, C ∈ L(y) = L (t). Assume s ∈ S 1 , i.e., s = ϕ(x) with x = pred i (x ), i ≥ 1 for some x ∈ I ∪ B.

Similarly.

-P13 holds due to the non-applicability of o ϕ -rule.

-P14 holds due to the construction of

T = {T o | o ∈ C o }.
-P15 holds due to the non-applicability of -rule.

Lemma 4 (Completeness) Let (T , R) be a SHOIQ knowledge base. If there is a tableau for (T , R) then Algorithm 3 answers "YES" by yielding a clash-free and complete set of SHOIQ-trees for (T , R).

Proof Let T = (S, L , E) be a tableau for (T , R). Let {T o = (V o , E o , L o , x o , • =) | o ∈ C o }
be a set of SHOIQ-trees. We show that there exists a sequence of expansion rule applications such that it generates a set of clash-free SHOIQ-trees with a partitioning function ϕ (**).

We maintain a function π from o∈Co V o to S such that they satisfy the following condition, denoted by (*):

(C1) L(x ) ⊆ L (π(x)) for all x ∈ ϕ(x), (C2) If y is a S-neighbour of x for some x ∈ ϕ(x) and y ∈ ϕ(y) then π(x), π(y) ∈ E(S), (C3) x • =y implies π(x) = π(y), (C4) y, y ∈ ϕ(x) implies π(y) = π(y ).

To prove (**), we have to show that (i) we can apply expansion rules to build a set of SHOIQ trees such that the conditions in (*) are preserved, and (ii) if the conditions (*) are satisfied when constructing SHOIQ trees by expansion rules then the set of obtained SHOIQ trees is clash-free.

According to P14 in Definition 4, for each o ∈ C o there is some This implies that NN ϕ -rule can be applied such that (*) holds. 9. For o ϕ -rule, assume that there are x, y such that o ∈ L(x) ∩ L(y) and ϕ(x) • =ϕ(y) does not hold. We have o ∈ L (π(x)) ∩ L (π(y)) due to (C1). This implies that π(x) = π(y) due to P13. Thus, L (π(x)) = L (π(y)). Moreover, it follows that L(x) ⊆ L (π(x)) and L(y) ⊆ L (π(x)) due to (C1). This implies that L(x ) ∪ L(y ) ⊆ L (π(x)) for all x ∈ ϕ(x) and y ∈ ϕ(y). Therefore, (C1) is preserved. It is obvious that (C2) and (C4) hold since π(x) = π(y). The condition (C3) holds since ϕ(y) • =ϕ(z) does not hold. Due to π(x) = π(y) and (*), (C4) is preserved as well. 10. ≤ ϕ -rule. If (≤ nS.C) ∈ L(x) then (≤ nS.C) ∈ L(x ) for all x ∈ ϕ(x) and (≤ nS.C) ∈ L (π(x)). Due to P10, card{S T (π(x), C)} ≤ n. The rule ≤ ϕ -rule is applicable if (i) there are (n + 1) nodes y 0 , • • • , y n such that C ∈ Λ(ϕ(y i )), S ∈ Λ( ϕ(x), ϕ(y i ) ) and ϕ(y i ) ∩ ϕ(y j ) = ∅ for all 0 ≤ i < j ≤ n. This implies that there are two nodes y, z ∈ {y 0 , • • • , y n } such that π(y) = π(z). Thus, ϕ(y) • =ϕ(z) cannot hold due to (*), and (ii) there are x , x ∈ ϕ(x) with

s o ∈ S such that o ∈ L (s o ). We initialize ϕ( x o ) = { x o } and π( x o ) = s o for each o ∈ C o . 1. -rule. Due to P1, we have nnf(¬C D) ∈ L (π(x)) for all x. Therefore, if nnf(¬C D) ∈ L(x ) for each x ∈ ϕ(x) then nnf(¬C D) ∈ L (π(x)) due to (
x = x such that x has a S-neighbour y ∈ ϕ(y) and x has a S-neighbour z ∈ ϕ(z) with C ∈ L(y ) ∩ L(z ). Therefore, ϕ(y), ϕ(z) and x , x can be chosen to merge by ≤ ϕ -rule. It is obvious that (C1) is preserved. If w is a R-neighbour of w with w ∈ ϕ(x ) ∪ ϕ(x ) and w ∈ ϕ(y ) ∪ ϕ(z ) then π(w), π(w ) ∈ E(R) due to π(y) = π(z) and (*). This implies (C2) holds. Moreover, (C3) is preserved since ϕ(y) • =ϕ(z) does not hold. Due to (*) and π(y) = π(z), (C4) is preserved as well.

It holds that ϕ is a partitioning function since the non-applicability of ≤ ϕ -rule. We now show that if the SHOIQ-trees and the partitioning function ϕ can be built with a function π satisfying (*) then T is clash-free.

1. T cannot contain a clash of the first kind due to (C1). 2. Assume that there are x • =y and o ∈ L(x) ∩ L(y) for some o ∈ C o . We have π(x) = π(y) due to P13. From (C3) it follows that x • =y does not hold, which is a contradiction. This implies that T cannot contain a clash of the second kind. 3. Assume that there is a node x ∈ o∈Co V o with (≤ nR.C) ∈ L(ϕ(x)) and there are (n + 1)

nodes x 0 , • • • , x n ∈ o∈Co V o such that ϕ(x i ) ∩ ϕ(x j ) = ∅, ϕ(x i ) • =ϕ(x j ) with i = j, and C ∈ L(ϕ(x i )), R ∈ L( ϕ(x), ϕ(x i ) ) for i ∈ {0, • • • , n}. By P10, there are x i , x j ∈ {x 0 , • • • , x n }, i = j such that π(x i ) = π(x j
). This implies that x i • =x j does not hold. For all x ∈ ϕ(x i ) and x ∈ ϕ(x j ) we have π(x ) = π(x i ) and π(x ) = π(x j ), and thus π(x ) = π(x ) due to (C4). This implies that x • =x does not hold due to (C3), which contradicts ϕ(x i ) • =ϕ(x j ).

The following theorem is the main result of the present section which is an immediate consequence of Lemmas 2, 3 and 4.

Theorem 6 Let (T , R) be a SHOIQ knowledge base. Algorithm 3 is a decision procedure for consistency of (T , R) and it runs in 2NEXPTIME in the size of (T , R).

6 A worst-case optimal algorithm for SHOIQ This section starts by translating results presented in [START_REF] Pratt-Hartmann | Complexity of the two-variable fragment with counting quantifiers[END_REF] for C 2 into those for SHOIQ.

Definition 8 (star-type) Let (T , R) be a SHOIQ knowledge base. A star-type is a triplet σ = λ σ , νσ , μσ , where R) , and νσ = ( r , l ) with r , l ∈ 2 R (T ,R) ×2 cl(T ,R) . A pair r, l is a ray of σ if r, l is a component of μσ or νσ . In particular, r, l is a predecessor ray if ( r, l ) = νσ , and r, l is a successor ray if r, l is a component of μσ . We denote ξσ = ( r 1 , l 1 , • • • , r d , l d , r d+1 , l d+1 ) if νσ = ( r , l ) where r = r d+1 , l = l d+1 , and ξσ = μσ if νσ is empty.

λ σ ∈ 2 cl(T ,R) , μσ = ( r 1 , l 1 , • • • , r d , l d ) is a d-tuple over 2 R (T ,R) ×2 cl(T ,
-A ray r , l of σ is primary w.r.t. a term

(≤ mR.C) if (≤ mR.C) ∈ λ σ , R ∈ r and C ∈ l . For a term (≤ mR.C) ∈ λ σ , we denote C σ ≤mR.C for the set of all rays r , l of σ such that R ∈ r , C ∈ l . -A star-type σ is nominal if o ∈ λ σ for some o ∈ C o .
-A star-type σ is chromatic if there is a term (≥ nS.D) ∈ λ σ and σ has n rays r 1 , l 1 , • • • , r n , l n such that S ∈ l i , D ∈ l i for all 1 ≤ i ≤ n, and l i = l j for all 0 ≤ i < j ≤ n with l 0 = λ σ .

-A star-type σ is homomorphic (resp. isomorphic) to a star-type σ if λ σ = λ σ , and for each term (≤ mR.C) ∈ λ σ , there is an injection (resp. a bijection) π : C σ ≤mR.C → C σ ≤mR.C such that π( r, l ) = r , l implies r = r and l = l. -Two star-types σ, σ are equivalent if λ σ = λ σ , and there is a bijection π between ξσ and ξσ such that π( r, l ) = r , l implies r = r and l = l.

We denote Σ for the set of all star-types for (T , R).

In the context of a SHOIQ-forest, we can think of a star-type σ as the set of nodes x such that L(x) = λ σ , and each ray r i , l i of σ corresponds to a neighbour x i of x such that L ( x, x i ) = r i and L(x i ) = l i . In this case, we say that x satisfies σ.

Remark 1 The notion of chromaticity introduced in Definition 8 implies an inequality relation • = over nodes. That stronger notion is needed to prevent "distinct" star-types from including nodes x, y which are neighbours or x • =y. In order to make star-types chromatic, it is necessary to add to knowledge bases some new concepts and axioms as follows. Let (T , R) be a SHOIQ knowledge base. For each term (≥ nS. ⊥ for all 0 ≤ i < j ≤ n. It is straightforward to prove that the terminology (T , R) is consistent iff (T , R) is consistent where T is obtained from T by adding these new axioms. Thanks to these new concepts and axioms, the following definition points out how to build chromatic star-types.

Definition 9 (valid star-type) Let (T , R) be a SHOIQ knowledge base. Let σ be a star-type for (T , R) where σ = λ σ , ν, μ with μ = ( r 1 , l 1 , • • • , r d , l d ) and λ σ = l 0 , ν = { r d+1 , l d+1 }. σ is valid if the following conditions are satisfied: 12. If (≤ nS.C) ∈ λ σ and there are no

1 ≤ i 1 < • • • < i n+1 ≤ d + 1 such that C ∈ l ij and S ∈ r ij for all 1 ≤ j ≤ n + 1;
We denote Σ for the set of all valid star-types for (T , R).

Notice that a valid star-type according to Definition 9 is chromatic. If we think of a star-type σ as a node x satisfying σ in a SHOIQ-forest then σ is valid if no expansion rule is applicable to x. Moreover, due to the conditions 7, 11 and 12 in Definition 9, if there is a term (≥ nS.D) ∈ λ σ for a valid star-type σ then σ has exactly n primary rays r i , l i , • • • , r n , l n w.r.t. (≤ nS.D).

Definition 10 (frame) Let (T , R) be a SHOIQ knowledge base. A frame for (T , R)

is a tuple F = (N 0 , • • • , N H ), δ, Φ , where -H ∈ N is the dimension of F; -N i ⊆ Σ for all 0 ≤ i ≤ H,
and all star-types in N 0 are nominal. We denote

N = i∈{1,••• ,H} N i ; -δ is a function δ : N → N; -Φ is a function Φ : N → 2 N
such that the following conditions are satisfied:

1. For each star-type σ ∈ N h with δ(σ) > 0, 0 ≤ h ≤ H, and for each ray r, l of σ, there are star-types σ 1 , • • • , σ k ∈ N l , and integers denoted by 0

< δ(σ, r, l , σ i ) ≤ δ(σ i ) (1 ≤ i ≤ k) where l = h -1 if r, l is a predecessor ray of σ and l = h + 1 if r, l is a successor ray of σ, such that -δ(σ) = 1≤i≤k δ(σ, r, l , σ i ), and
-each σ i (1 ≤ i ≤ k) has a ray r i , l i with l = λ σi , l i = λ σ and r = r - i where r - i = {R | R ∈ r i }. We denote Ω(σ, r, l ) = {σ 1 , • • • , σ k } and say that σ is linkable with σ 1 , • • • , σ k by r, l . 2.
For two star-types σ, σ ∈ N, if σ ∈ Φ(σ) then either σ is isomorphic to σ , or there is a star-type ω ∈ N \ N H such that σ and σ are homomorphic to ω.

Remark 2 For σ, σ / ∈ N H such that σ, σ are valid, if σ is homomorphic to σ then σ is isomorphic to σ . In fact, if there is a term (≤ mR.C) ∈ λ σ then both σ, σ have exactly m primary rays w.r.t. (≤ mR.C). If there is a homomorphism between the two sets of primary rays w.r.t. (≤ mR.C) then it is an isomorphism as well.

The frame structure, as introduced in Definition 10, allows us to tile a forest structure by star-types. Such a structure is crucial to obtain termination when designing a tableau-based algorithm. An important difference between a frame and a SHOIQ-forest is that a frame does not represent nodes corresponding to individuals but stores the number of individuals satisfying a star-type. The function δ(σ) is used for this purpose. The condition 1 in Definition 10 introduces the relation of linkability for star-types while the condition 2 provides a characteristic of Φ which regroups "specific" homomorphic star-types for representing a partition in the context of a SHOIQ-forest. Notice that the chromaticity of star-types prevents chromatically linakble star-types from collapsing into a unique star-type by the function Φ.

Definition 11 (valid frame) Let (T , R) be a SHOIQ knowledge base. A frame F = (N 0 , • • • , N H ), δ, Φ is valid if the following conditions are satisfied:

1. For each σ ∈ N, if δ(σ) ≥ 1 then σ is valid and σ ∈ Φ(σ); 2. For each o ∈ C o there is a star-type σ ∈ N 0 such that o ∈ λ σ and δ(σ) = 1; 3. For two star-types σ, σ ∈ N with δ

(σ) ≥ 1, δ(σ ) ≥ 1, if o ∈ λ σ ∩ λ σ with some o ∈ C o then σ ∈ Φ(σ); 4. For each 0 ≤ k < H and λ, r, λ ∈ 2 cl(T ,R) × 2 R (T ,R) × 2 cl(T ,R) with r -= {R | R ∈ r}, σ∈N k δ(σ)|μ σ | λ,r,λ = σ ∈N k+1 δ(σ )|ν σ | λ ,r -,λ
where |ν σ | λ,r,λ and |μ σ | λ,r,λ are denoted for the number of components r , l of respective νσ and μσ such that λ σ = λ, r = r and l = λ ; 5. For two star-types σ, σ ∈ Φ(σ ) which have respective primary ray r, l and r , l w.r.t. (≤ m.R.C) such that r = r and l = l , if there are two star-types ω, ω ∈ N such that σ and σ are linkable with respective ω and ω by r, l and r , l then ω ∈ Φ(ω ).

The notion of validity for a frame is crucial to establish a connection with the tableau-based algorithm presented in Section 5, i.e., how to build a SHOIQ-forest from a valid frame, and inversely. The condition 1 in Definition 11 requires that every star-type satisfied by at least one node must be valid. The condition 2 ensures that each nominal is counted exactly once by δ while the condition 3 imposes that all nominal star-types containing some o ∈ C o are regrouped into a unique partition of star-types by Φ. In the context of a SHOIQ-forest, these conditions imply that for each nominal o ∈ C o there is exactly one tree whose root contains o and there is exactly one partition containing o. The condition 4 allows for linking star-types at level k with star-types at level k-1 and k+1. It ensures that each node x satisfying (or counted for) a star-type σ at level k is linked by its rays to neighbours satisfying startypes at level k -1 and k + 1. The number of these neighbours corresponds exactly to the number of σ's rays. Finally, the condition 5 deals with partitions. The definition of Φ is based on the two following notions : homomorphism and linkability. That means that from a partition Φ(σ) of star-types we can build a "neighbour" partition Φ(σ ) including homomorphic star-types which are linkable with star-types included in Φ(σ). Notice that in the context of a SHOIQ-forest, the definition of Φ does not imply that two nodes satisfying a star-type belong to a partition of nodes.

Lemma 5 Let (T , R) be a SHOIQ knowledge base.

1. If Algorithm 3 can build a clash-free SHOIQ-forest for (T , R) then there is a valid frame for (T , R).

If there is a valid frame

F = (N 0 , • • • , N H ), δ, Φ for (T , R) then Algorithm 3
can build a clash-free SHOIQ-forest for (T , R).

Proof • Assume that Algorithm 3 builds a clash-free SHOIQ-forest G = T, ϕ for (T , R). To obtain a frame whose dimension H = max{h(pred(x)) | x is blocked}

Input : A SHOIQ knowledge base (T , R) Output: Is (T , R) consistent ?
Guess a number H with H ≤ K where K = 2 2m+k × 2 with m = card{cl(T , R)} and

1 k = card{R (T ,R) };
For each σ ∈ Σ, guess a number δ(σ) < M For each level, we regroup nodes x which satisfy a same star-type σ (i.e. all x have a same label, and for each ray r, l of σ, x has a unique neighbour y such that L ( x, y ) = r and l = L(y)). We denote σ(x) = σ if x is regrouped into σ. This allows us to determine δ(σ) for each σ ∈ N k where N k is the set of all star-types at level k of G, k ≤ 2 (2m+k) × 2. Moreover, we can define that σ(x) is linkable with σ(x ) by a ray r, l iff x is a neighbour of x such that L ( x, x ) = r and L(x ) = l. From the defined star-types σ(x), we can define a function Φ as follows:

-We initialize Φ(σ(x)) := {σ(x)} for each node x; -For each node x with o ∈ L(x) ∩ C o , we define Φ(σ(x)) = x ∈ϕ(x) Φ(σ(x ))
-For each Φ(σ(w)) and for each s, λ ∈ 2 R (T ,R) × 2 cl(T ,R) such that there is a star-type σ(x) ∈ Φ(σ(w)) which has a primary ray r, l with r = s and l = λ, we define Φ(σ(y)) to be the union of all Φ(σ(y )) such that there is a star-type σ(x ) ∈ Φ(σ(w)) which is linkable with σ(y ) by a primary ray r , l with r = s and l = λ.

By the definition of Φ and the construction of G, it holds that x ∈ ϕ(x) implies σ(x ) ∈ Φ(σ(x)). Moreover, Φ satisfies the condition 2 in Definition 10 since σ(x ) ∈ Φ(σ(x)) implies that either σ(x ) is isomorphic to σ(x) (if x, x are simultaneously blocked or non-blocked), or σ(x) is homomorphic to σ(x ) (if x is blocked). It is trivial to show that Φ satisfies the conditions 1, 3 and 5 in Definition 11. Let 0 ≤ k < H such that for each i < k and for each star-type σ ∈ N i there are δ(σ ) nodes added to T o with δ(σ ) > 0. Due to the condition 2 in Definition 10 and the condition 4 in Definition 11, there are ω 1 , • • • , ω h ∈ N k+1 and integers 0 < α(σ, r, l , ω i ) ≤ δ(ω i ) such that λ ωi = l, r -, λ σ k ∈ ν(ω i ) and 1≤i≤h α(σ, r, l , ω i ) = δ(σ(x)). For each ω i with 1 ≤ i ≤ h, we add α(σ, r, l , ω i ) successors y j of x such that σ(y j ) = ω i and define L(y j ) = λ ωi , L( x, y j ) = r for 1 ≤ j ≤ α(σ, r, l , ω i ).

• Assume that F = (N 0 , • • • , N H ), δ, Φ
Let Ψ be a set of all nodes x added from level 0 to level k. We define a partitioning function ϕ over Ψ as follows:

x ∈ ϕ(x); -If o ∈ L(x) ∩ L(x ) for some o ∈ C o then x ∈ ϕ(x); -For x , x ∈ ϕ(x) which have neighbours y , y such that Φ(σ(x)) has a primary ray r, l with L ( x , y ) = r, L ( x , y ) = r, L(y ) = l and L(y ) = l, if Φ(σ(y )) = Φ(σ(y )) then y ∈ ϕ(y ).

We show that x ∈ ϕ(x) implies Φ(σ(x )) = Φ(σ(x)) (*). Assume that x ∈ ϕ(x), Φ(σ(x )) = Φ(σ(x)) and (≤ mR.C) ∈ λ σ(x) . Let y, y be two R-neighbours of respective x, x such that C ∈ L(y) ∩ L(y ), L(y) = L(y ) and L ( x, y ) = L ( x , y ). Since σ(x ), σ(x) are linkable with σ(y ), σ(y), by the the condition 5 in Definition 11, we have Φ(σ(y)) = Φ(σ(y )).

Let x be a non-blocked node such that σ(x) ∈ N k and σ(pred 1 (x)) ∈ N k-1 . Let r, l be a component of μ(σ(x)). We will define successors of x.

-Assume that there is no term (≤ mR.C) ∈ λ σ(x) with R ∈ r, C ∈ l.

-Assume that C o ∩ l = ∅. We define ϕ(y j ) := {y j }. Assume that there is a term (≤ mR.C) ∈ l with R ∈ r -, C ∈ L(x). Since ϕ(y j ) has a unique neighbour partition ϕ(x) and m > 0, the condition 5 in Definition 6 holds. -Assume that o ∈ C o ∩ l. We define ϕ(y ) := ϕ( x o ) ∪ {y j } for each y ∈ ϕ( x o ) ∪ {y j }.

Assume that there is a term (≤ mR.C) ∈ l with R ∈ r -, C ∈ L(x). We will show that ϕ( . This implies x ∈ ϕ(w k ) according to the definition of ϕ as described above. Thus, the condition 5 in Definition 6 holds. -Assume that there is a term (≤ mR.C) ∈ λ σ(x) with R ∈ r, C ∈ l.

-Assume that C o ∩ l = ∅. Assume that there is no node w = x that was added to T o at a level i ≤ k such that w ∈ ϕ(x). We define ϕ(y j ) := {y j }. It follows that ϕ(x) has at most m R-neighbour partitions containing C since σ(x) has m primary rays w.r.t. (≤ mR.C). Assume that there is a term (≤ nS.D) ∈ L(y j ) with R ∈ r -, C ∈ L(x). In this case, ϕ(y j ) has at most n > 0 S-neighbour partitions containing D since ϕ(y j ) has a unique neighbour partition ϕ(x).

Assume that there is a node w = x that was added to T o at a level i ≤ k such that w ∈ ϕ(x) and w has a R-neighbour w such that containing C such that L(w ) = L(y j ) and L ( w, w ) = L ( x, y j ). This implies that σ(w) and σ(x) are linkable with respective σ(w ) and σ(y j ). According to (*) we have σ(w) ∈ Φ(σ(x)). By the condition 5 in Definition 11, we have σ(w ) ∈ Φ(σ(y j )). According to the definition of ϕ as described above, we have ϕ(y j ) = ϕ(w ) ∪ {y j }. This implies that the condition 5 in Definition 6 holds. -Assume that o ∈ C o ∩ l. Due to the condition 3 in Definition 11, we have σ(y j ) ∈ Φ(σ( x o )) where x o is the root of T o . We define ϕ(y ) := ϕ( x o ) ∪ {y j } for each y ∈ ϕ( x o ) ∪ {y j }.

Assume that there is no node w = x that was added to T o at a level i ≤ k such that w ∈ ϕ(x). It follows that ϕ(x) has at most m R-neighbour partitions containing C since σ(x) has m primary rays w.r.t. (≤ mR.C). Assume that there is a term (≤ nS.D) ∈ L(y j ) with R ∈ r -, D ∈ L(x). By the condition 5 in Definition 11, we have σ(x) ∈ Φ(σ(w i )) where w i is successor of x o such that L(w i ) = L(x) and L ( y j , x ) = L ( x o , w i ). According to the definition of ϕ as described above, we have ϕ(x) = ϕ(w i ). This implies that the condition 5 in Definition 6 holds. Assume that there is a node w = x that was added to T o at a level i ≤ k such that w ∈ ϕ(x) and w has a R-neighbour w such that containing C such that L(w ) = L(y j ) and L ( w, w ) = L ( x, y j ). According to (*) we have σ(w) ∈ Φ(σ(x)). By the condition 5 in Definition 11, we have σ(w ) ∈ Φ(σ(y j )). According to the definition of ϕ as described above, we have ϕ(y j ) = ϕ(w ) ∪ {y j }. This implies that the condition 5 in Definition 6 holds.

This process of construction terminates at a node x when the blocking condition for a SHOIQ-forest is satisfied for x. Notice that the blocking condition for a frame implies the blocking condition for SHOIQ-forests. By the construction of T o and ϕ as described above, the conditions 1-5 in Definition 6 hold. In particular, the condition 6 in Definition 6 is a consequence of the chromaticity of star-types, Lemma 6 Let (T , R) be a SHOIQ knowledge base. The size of a valid frame F = (N 0 , • • • , N H ), δ, Φ is bounded by an exponential function in the size of (T , R).

Proof We have H ≤ K where K = 2 2m+k × 2 with m = card{cl(T , R)} and k = card{R (T ,R) }. Moreover, each valid star-type has at most M distinct rays where M = m i +E, m i occurs in a number restriction term (≥ m i R.C) appearing in T , and E is the number of distinct terms ∃R.C appearing in T . If we denote Σ for the set of all star-types then card{Σ} ≤ (card{cl(T , R)}) 2 × card{R (T ,R) }) M . Since δ(σ) is bounded by M δ(σ ) where σ , σ are respective star-types at level k -1 and k, it holds that δ(σ) ≤ M 2 2m+k ×2 . If δ(σ) is represented as a binary number then it takes an exponential number of bits. In addition, since the function Φ partitions N we have the number of partitions is bounded by card{N} where N = i∈{1,••• ,H} N i .

In addition, for each σ ∈ N and for each ray r, l of σ, the cardinality of two sets N (σ, r, l ) and N (σ, r, l ) of linkable star-types is bounded by card{N}.

The following theorem affirms that we can obtain a worst-case optimal algorithm for SHOIQ which is founded on Lemma 5 and 6.

Theorem 7 Let (T , R) be a SHOIQ knowledge base. Algorithm 4 is a decision procedure for consistency of (T , R) and it runs in NEXPTIME.

Proof According to Theorem 7, (T , R) is consistent iff there is a clash-free SHOIQforest T, ϕ . Due to Lemma 5 and 6, it suffices to show that all conditions in Definition 10 and Definition 11 can be checked exponentially. In fact, checking the condition 1 in Definition 10 for linkability is exponentially since the cardinality of two sets N (σ, r, l ) and N (σ, r, l ) of linkable star-types is bounded by card{N}. Moreover, since Φ partitions the set of all star-types, the number of distinct Φ(σ) is bounded by card{N} where N = i∈{1,••• ,H} N i .

Since we have at most an exponential number of distinct star-types, an exponential number of distinct triplet λ, r, λ ∈ 2 cl(T ,R) × 2 R (T ,R) × 2 cl(T ,R) , checking the conditions in Definition 11 is exponential.

Conclusion and Discussion

We have presented in this paper a practical EXPSPACE decision procedure for the logic SHOIQ. The construction of this algorithm is founded on the well-known results for SHOIQ and C 2 . First, we have based our approach on a technique that constructs tree-like structures for representing a model. This allows us to reuse the standard blocking technique over these tree-like structures to obtain termination. Second, we have transferred to SHOIQ the method used for constructing a NEXPTIME algorithm for C 2 . This enables us to represent a double exponential SHOIQ-forest by an exponential structure. This result allows us to devise a worst-case optimal algorithm for deciding consistency of a SHOIQ knowledge base.

  r.t. R if Trans(Q) = false. * An interpretation I = (∆ I , • I ) consists of a non-empty set ∆ I (domain) and a function • I which maps each role name to a subset of ∆ I × ∆ I such that R -I = { x, y ∈ ∆ I × ∆ I | y, x ∈ R I } for all R ∈ R, and x, z ∈ S I , z, y ∈ S I implies x, y ∈ S I for each S ∈ R + An interpretation I satisfies a role hierarchy R if R I ⊆ S I for each R S ∈ R. Such an interpretation is called a model of R, denoted by I |= R.

Definition 2 (

 2 terminology) Let C be a non-empty set of concept names with a nonempty subset C o ⊆ C of nominals. * The set of SHOIQ-concepts is inductively defined as the smallest set containing all C in C, , C D, C D, ¬C, ∃R.C, ∀R.C, (≤ n S.C) and (≥ n S.C) where n is a positive integer, C and D are SHOIQ-concepts, R is an SHOIQ-role and S is a simple role w.r.t. a role hierarchy. We denote ⊥ for ¬ . * The interpretation function • I of an interpretation I = (∆ I , • I ) maps each concept name to a subset of ∆ I such that I = ∆ I , (C D) I = C I ∩ D I , (C D) I = C I ∪ D I , (¬C) I = ∆ I \C I , card{o I } = 1 for all o ∈ C o , (∃R.C) I = {x ∈ ∆ I | ∃y ∈ ∆ I , x, y ∈ R I ∧ y ∈ C I }, (∀R.C) I = {x ∈ ∆ I | ∀y ∈ ∆ I , x, y ∈ R I ⇒ y ∈ C I }, (≥ n S.C) I = {x ∈ ∆ I | card{y ∈ C I | x, y ∈ S I } ≥ n}, (≤ n S.C) I = {x ∈ ∆ I | card{y ∈ C I | x, y ∈ S I } ≤ n} where card{S} is denoted for the cardinality of a set S. * C D is called a general concept inclusion (GCI) where C, D are SHOIQconcepts (possibly complex), and a finite set of GCIs is called a terminology T . * An interpretation I satisfies a GCI C D if C I ⊆ D I and I satisfies a terminology T if I satisfies each GCI in T . Such an interpretation is called a model of T , denoted by I |= T . Definition 3 (knowledge base) A pair (T , R) is called a SHOIQ knowledge base where R is a SHOIQ role hierarchy and T is a SHOIQ terminology. * A knowledge base (T , R) is said to be consistent if there is a model I of both T and R, i.e., I |= T and I |= R. * A concept C is called satisfiable w.r.t. (T , R) iff there is some interpretation I such that I |= R, I |= T and C I = ∅. Such an interpretation is called a model of C w.r.t. (T , R). * A concept D subsumes a concept C w.r.t. (T , R), denoted by C D, if C I ⊆ D I holds in each model I of (T , R).

  • = o y for some o ∈ C o ; 3. For all ϕ(x) and ϕ(x ), if there are two edges y, y ∈ E o and w, w ∈ E o with o, o ∈ C o such that y, w ∈ ϕ(x), y , w ∈ ϕ(x ) and L ( y, y ) = ∅, L ( w, w ) = ∅ then L ( y, y ) = L ( w, w ).

and 3 .

 3 there are x , x ∈ ϕ(x) with x = x , and x has a R-neighbour y , x has a R-neighbour y s.t. C ∈ L(y ) ∩ L(y ), ϕ(y ) ∩ ϕ(y ) = ∅, and not ϕ(y ) • =ϕ(y ) then 1. Propagate(ϕ(y ), ϕ(y ), ϕ(x)), 2. ϕ(y) = ϕ(y ) ∪ ϕ(y ) for all y ∈ ϕ(y ) ∪ ϕ(y ).

Figure 2 :

 2 Figure 2: New expansion rules for SHOIQ

Input : A 1 L 4 if 8 Algorithm 3 :

 A1483 SHOIQ knowledge base (T , R) Output: Is (T , R) consistent ? For each o ∈ Co, let To = (Vo, Eo, Lo, xo, • =o) be an initial tree such that Vo = { xo}, ( xo) = {o}, and there are no x, y ∈ Vo such that x • =y; A partitioning function ϕ is initialized with ϕ( xo) = { xo} ; 2 while there is a non-empty set S of expansion rules in Figure 1 and 2 such that each r ∈ S can be 3 applied to a node x ∈ Vo do Apply r to x ; there is a clash-free set of trees {To | o ∈ Co} then A 2EXPSPACE algorithm for checking consistency of a SHOIQ knowledge base

Definition 7 (

 7 Innerness and unravelling) Let T = {T o | o ∈ C o } and ϕ be a set of SHOIQ-trees and a partitioning function, respectively, which are built by Algorithm 3 for a SHOIQ knowledge base (T , R) where

  1. b(x) has a nominal descendant z with b(x) = pred k (z) and each node y = pred k (z) for k ≤ k ≤ 0 is inner. This implies that b(x) is inner and b(x) is an ancestor of x, which is a contradiction. 2. b(x) has a blocked descendant y such that b(y ) = pred m (b(x)) (m > 0), b(y ) has a nominal descendant z with b(y ) = pred l (z ) (l > 0) and each node w = pred l (z ) for 0 < l ≤ l is inner. This implies b(y ) is inner and b(y ) is an ancestor of x, which is a contradiction.

  Figure 2 illustrates graphically the construction of T. First, it initializes L( x o ) = {o} and ϕ( x o ) = { x o }. Then, by applying -rule and -rule to x o , we have : L( x o ) ⊇ {o, ∃S.o, (¬C ∃F.C ∀R.∃F.C), ∃S.o, ¬C, ∃F.C, ∀R.∃F.C} In turn, ∃-, ∀-, ∀ + -and -rule are applied to x o to obtain two new nodes y 0 and x 1 such that L( x o , y 0 ) = {S}, L( x o , x 1 ) = {R, F }, ϕ(y 0 ) = {y 0 }, ϕ(x 1 ) = {x 1 } and L(y 0 ) ⊇ {o, ∃S.o, (¬C ∃F.C ∀R.∃F.C)}, L(x 1 ) ⊇ {C, ∃F.C, ∀R.∃F.C, ∃S.o, ¬o}. Then, -rule is applied to y 0 and x 1 , we have L(y 0 ) ⊇ {o, ∃S.o, (¬C ∃F.C ∀R.∃F.C), ¬C, ∃F.C, ∀R.∃F.C}, L(x 1 ) ⊇ {C, ∃F.C, ∀R.∃F.C, ∃S.o, ¬o}.

  x o and y i for i ∈ {0, • • • , 4} in order to obtain ϕ( x o ) = ϕ(y 0 ) = • • • = ϕ(y 4 ) = { x o , y 0 , • • • , y 4 }. No label propagation is needed. Application of o ϕ -rule yields an edge ϕ( x o ), ϕ( x o ) with Λ( ϕ( x o ), ϕ( x o ) ) = {S} since there is an edge x o , y 0 with x o , y 0 ∈ ϕ( x o ).

  each ϕ(x) with x ∈ B ∩ V o and o ∈ C o , we define an infinite tree T ϕ(x) o and a function p (stand for Projection) from the nodes of T ϕ(x) o to V o as follows :

  ϕ(x) o and ∃S.C ∈ L (s). We consider the following cases: s = b 1 (ϕ(y)) for some y ∈ B. This implies that ∃S.C ∈ L(b(y)). Due to the non-applicability of ∃-rule, b(y) has a S-neighbour y with C ∈ L(y ). If y is a successor of b(y), by the definition of V ϕ(x) o

  C1). Moreover, -rule adds nnf(¬C D) to L(x ) for all x ∈ ϕ(x) i.e. (C1) is preserved. Since (C2) and (C3) are trivially preserved, (*) holds if -rule is applied.2. -rule. Due to P3, if (C D) ∈ L (π(x)) then {C, D} ⊆ L (π(x)). Due to (*) if (C D) ∈ L(x ) then (C D) ∈ L (π(x)) for all x ∈ ϕ(x). Moreover, -rule adds C, D to L(x ) for all x ∈ ϕ(x) if (C D) ∈ L(x ) i.e. (C1) is preserved. Since (C2) -(C4) are trivially preserved, (*) holds if -rule is applied. 3. -rule. Due to P4, if (C D) ∈ L (π(x)) then {C, D} ∩ L (π(x)) = ∅. Due to (*) if (C D) ∈ L(x ) then (C D) ∈ L (π(x)) for all x ∈ ϕ(x). Therefore, -rule can add a concept E ∈ {C, D} to L(x ) such that L(x ) ⊆ L (π(x)) for all x ∈ ϕ(x) i.e. (C1) is preserved. Since (C2) -(C4)are trivially preserved, (*) holds if -rule is applied. 4. Analogously, we can show ∀-rule, ∀ + , ch-rule can be applied such that (*) holds. 5. ∃-rule. If ∃S.C ∈ L(x) then ∃S.C ∈ L(x ) for all x ∈ ϕ(x) and ∃S.C ∈ L (π(x)). Due to P7, if ∃S.C ∈ L (π(x)) there is an individual t such that π(x), t ∈ E(S) and C ∈ L (t). The application of ∃-rule create a new node y such that L(y) = {C} and L( x, y ) = {S}. We set π(y) = t and ϕ(y) = {y}. This implies that (C2) -(C4) are preserved. Thus, (*) holds if ∃-rule is applied. 6. Analogously, we can show ≥-rule can be applied such that (*) holds. 7. ≤-rule.If (≤ nS.C) ∈ L(x) then (≤ nS.C) ∈ L(x ) for all x ∈ ϕ(x) and (≤ nS.C) ∈ L (π(x)). Due to P10, card{S T (π(x), C)} ≤ n. The ≤-rule is applicable if x has (n + 1) S-neighbours y 0 , • • • , y n with C ∈ L(y i ). Due to (C3) -(C4) there are y, z ∈ {y 0 , • • • , y n } such that ϕ(y) = ϕ(z)and y • =z does not hold. Therefore, y, z can be chosen to merge by ≤-rule where y is a successor of x. It is obvious that (C1) is preserved. If y was a R-neighbour of x then z is now a R-neighbour of x and π(x), π(z) ∈ E(R) due to π(y) = π(z) and (*). This implies that (C1) -(C2) hold. Moreover, (C3) is preserved since ϕ(y) • =ϕ(z) does not hold. Due to (*) and π(y) = π(z), (C4) is preserved as well. 8. For NN ϕ -rule, assume that (≤ nS.C) ∈ L(x) with n > 0. If (≤ nS.C) ∈ L(x) then (≤ nS.C) ∈ L(x ) for all x ∈ ϕ(x) and (≤ nS.C) ∈ L (π(x)). By P15, we have {≤ mS.C, ≥ mS.C} ⊆ L (π(x)) with 1 ≤ m ≤ n.

  D) ∈ cl(T , R), we add to cl(T , R) n new concept names C 0 (≥nS.D) , • • • , C n (≥nS.D) , and to T the following axioms: C i (≥nS.D) C j (≥nS.D)

  is a valid frame for (T , R). Due to the condition 2 in Definition 11, for each o ∈ C o there is a unique star-type σ o ∈ N 0 such that o ∈ λ σo and δ(σ o ) = 1. For each σ o we add a root node x o to a tree T o with L o ( x o ) = λ σo . We initialize ϕ( x o ) = { x o }. We denote σ(x) := σ for each node x added to T o such that x satisfies σ.

  x o ) has m R neighbour partitions containing C. By construction, x o has m R-successors w 1 , • • • , w m containing C. Due to the chromaticity, it follows that Φ(σ(w i )) = Φ(σ(w i )) for all 1 ≤ i < i ≤ m. Moreover, due to the condition 3 in Definition 11, we have Φ(σ(y j )) = Φ(σ( x o )). By the condition 2 in Definition 10, σ(y j ) is homomorphic to σ( x o ). This implies that there is some 1 ≤ k ≤ m such that L(w k ) = L(x) and L ( x o , w k ) = L ( y j , x ). By the condition 5 in Definition 11, we have Φ(σ(x)) = Φ(σ(w k ))

  2 2m+k ×2 where M = m i + E, m i occurs in a 2 number restriction term (≥ m i R.C) appearing in T , and E is the number of distinct terms ∃R.C appearing in T ; Build a frame F = (N 0 , • • • , N H ), δ, Φ for (T , R) with the guessed H and δ(σ) for σ ∈ Σ; An optimal worst-case algorithm for checking consistency of a SHOIQ knowledge base where h(y) is denoted for the level of a node y, we can extend each tree T o ∈ T by unravelling each blocked node x until the level H (cf. the proof of Lemma 3).

	3
	4	if F is valid then
	5	return YES ;
	6	else
		return NO ;

7

Algorithm 4: