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

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

Olivier Curé

An ExpSpace Tableau-based Algorithm for SHOIQ

come

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]. An interesting feature of logics with nominals (denoted by O in SHOIQ) 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.

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, tableaux-based algorithms presented in [START_REF] Horrocks | The even more irresistible SROIQ[END_REF] for SHOIQ have been exploited to implement reasoners such as 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 [START_REF] Horrocks | The FaCT system[END_REF].

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.

Our approach is inspired from a technique that was employed by Ian Pratt-Hartmann in [START_REF] Pratt-Hartmann | Complexity of the two-variable fragment with counting quantifiers[END_REF] to construct a NEXPTIME algorithm for the logic C 2 including SHOIQ. Unlike the existing tableaux-based 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 describes a 2EXPSPACE tableaux-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 4 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 the these results, we propose an EXPSPACE tableaux-based algorithm for SHOIQ. Finally, we discuss the results and future work.

For the lack of place, we refer the reader to [START_REF] Duc | An EXPSPACE tableaux-based algorithm for SHOIQ[END_REF] for examples and full proofs.

The Description Logic SHOIQ

In this section, we present the syntax and the semantics 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-neighbour of s.

Q ∈ R + ∪{P ⊖ | P ∈ R + } such that Q * ⊑R. A role R is called simple w.r.t. R if Trans(Q) =
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 } ≤
C ⊑ D, if C I ⊆ D I holds in each model I of (T , R).
Thanks to the reductions between unsatisfiability, subsumption of concepts and knowledge base consistency, it suffices to study knowledge base consistency.

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 SHOIQ-concept 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]. 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 can define a set cl(T , R). For the sake of brevity, we refer the reader to [START_REF] Horrocks | A tableau decision procedure for SHOIQ[END_REF] for a more complete definition.

To prove soundness and completeness of our algorithms, we need a tableau structure that represents a model of a SHOIQ knowledge base. 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-neighbour individuals t of s if (≤ nS.C) ∈ L(s). This property makes explicit nondeterminism implied from the semantics of (≤ nS.C) and requires an extra expansion rule, namely ⊲⊳-rule, introduced in Figure 1 (Appendix). The presence of this rule may have an impact on the so-called "pay-asyou-go" behaviour of the tableaux-based algorithm presented in this paper.

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

It is not hard to prove that there is a tableau with the new property P15 for a SHOIQ knowledge base (T , R) iff (T , R) is consistent. A proof of a similar result 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].

A 2EXPSPACE decision procedure for SHOIQ

In this section, we introduce a structure, called SHOIQ-forest. We will show that such a forest is sufficient to represent a model of a SHOIQ-knowledge base.

Definition 4 (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 defined 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 .
= 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-neighbours as follows: :

S To (x, C) = {y ∈ V o | y is a S-neighbour 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 : (i)

x o = pred n (y), y = pred m (x), (ii) x ′ = pred 1 (x), y ′ = pred 1 (y), (iii) L o (x) = L o (y), L o (x ′ ) = L o (y ′ ), (iv) L o ( x ′ , x ) = L o ( y ′ , y )
, and (v) 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
= 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 4 for SHOIQtrees is very similar to the standard definition of blocked nodes for SHIQ completion 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 4 are also blocked nodes according to the standard definition for this SHIQ completion tree.

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.

Definition 5 (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 de- note Λ(ϕ(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 • = 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 ′ ).
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 (i) ϕ(x i ) ∩ ϕ(x j ) = ∅ for all 0 ≤ i < j ≤ n, and (ii) C ∈ Λ(ϕ(x i )), R ∈ Λ( ϕ(x), ϕ(x i ) ) for all i ∈ {0, • • • , n}, then ϕ(x l ) • =ϕ(x m ) for all 0 ≤ l < m ≤ 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}.
We now describe the tableaux-based algorithm whose goal is to construct from a knowledge base (T , R) a SHOIQ-forest G = T, ϕ . To do this, the algorithm applies the expansion rules as described in Figure 1 and 2 (Appendix), 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:

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 (i) if z ′ is a successor of w ′ and S / ∈ L( w ′ , z ′ ) then L( w ′ , z ′ ) = L( w ′ , z ′ ) ∪ {S}, (ii) if w ′ is a successor of z ′ and S / ∈ L( z ′ , w ′ ) then L( z ′ , w ′ ) = L( z ′ , w ′ ) ∪ {S ⊖ }.
The rules in Figure 1 (Appendix) 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 Figure 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. By the ⊲⊳-rule in Figure 2, each node x containing a term (≤ nS.C) has exactly m S-neighbours 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 "mergingand-generating" without pruning nodes since all merges due to number restrictions or nominals are performed by updating the partitioning function.

The following lemma establishes correctness and completeness of the algorithm.

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

1. The tableaux algorithm terminates and builds a SHOIQ-forest whose the size is bounded by a double exponential function in the size of (T , R).

If the tableaux algorithm yields a clash-free and complete SHOIQ-forest for

(T , R) then there is a tableau for (T , R). 3. If there is a tableau for (T , R) then the tableaux algorithm yields a clash-free and complete SHOIQ-forest for (T , R).

It is straightforward to show that the size of a SHOIQ-forest is bounded by a double exponential function in the size of (T , R). To prove soundness of the tableaux algorithm, we can devise a model from a clash-free and complete SHOIQ-forest by considering a partition as an individual and unraveling blocked nodes since we can show that each blocking node b(x) has no "core path" from b(x) to every nominal descendant y, i.e., there do not exist terms

(≤ m i R i .C i ) ∈ pred i (y), roles R i ∈ L( pred i-1 (y), pred i (y) ) and concepts C i ∈ L(pred i+1 (y)) for k < i ≤ 0 with b(x) = pred k (y).
The following theorem is a consequence of Lemma 1.

Theorem 1. Let (T , R) be a SHOIQ knowledge base. The tableaux algorithm is a decision procedure for consistency of (T , R) and it runs in 2NEXPTIME in the size of (T , R).

An EXPSPACE tableaux-based algorithm for SHOIQ

This section starts by translating from 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 6 (star-type). Let (T , R) be a SHOIQ knowledge base. A star-type is a triplet σ = λ σ , νσ , μσ , where λ σ ∈ 2 cl(T ,R) , νσ contains at most a pair r, l ∈ 2 R (T ,R) × 2 cl(T ,R) and μσ = (

r 1 , l 1 , • • • , r dσ , l dσ ) is a d-tuple over 2 R (T ,R) × 2 cl(T ,R) . A pair r ′ , l ′ is a ray of σ if r ′ , l ′ is a component of μσ or r ′ , l ′ ∈ νσ . We define an inequality relation • = over the set of rays. A ray r ′ , l ′ of σ is primary w.r.t. a term (≤ mR.C), denoted r ′ , l ′ ≤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 isomorph to a star-type σ ′ if λ σ = λ σ ′ ,
and for each term (≤ mR.C) ∈ λ σ , there is an injection π :

C σ ≤mR.C → C σ ′ ≤mR.C such that π( r, l ) = ( r, l ). -Two star-types σ, σ ′ are isomorph if λ σ = λ σ ′ , and for each term (≤ mR.C) ∈ λ σ ,
there is a bijection π :

C σ ≤mR.C → C σ ′ ≤mR.C such that π( r, l ) = ( r, l ). -A star-type σ = λ, ν, μ 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: 1. If C ⊑ D ∈ T then nnf(¬C ⊔ D) ∈ l i for all 0 ≤ i ≤ d σ + 1; 2. {A, ¬A} ⊆ l i for every concept name A with 0 ≤ i ≤ d σ + 1; 3. If C 1 ⊓ C 2 ∈ l i then {C 1 , C 2 } ⊆ l i for all 0 ≤ i ≤ d σ + 1; 4. If C 1 ⊔ C 2 ∈ l i then {C 1 , C 2 } ∩ l i = ∅ for all 0 ≤ i ≤ d σ + 1;
5. If ∃R.C ∈ λ then there is some 1 ≤ i ≤ d σ + 1 such that C ∈ l i and R ∈ r i ; 6. If (≤ nS.C) ∈ λ and there is some

1 ≤ i ≤ d σ + 1 such that S ∈ r i then C ∈ l i or ¬C ∈ l i ; 7. If (≤ nS.C) ∈ λ and there is some 1 ≤ i ≤ d σ +1 such that C ∈ l i and S ∈ r i then there is some 1 ≤ m ≤ n such that {(≤ mS.C), (≥ mS.C)} ⊆ λ; 8. For each 1 ≤ i ≤ d σ + 1, if R ∈ r i and R * ⊑S then S ∈ r i ; 9. If ∀R.C ∈ λ and R ∈ r i for some 1 ≤ i ≤ d σ + 1 then C ∈ l i ; 10. If ∀R.D ∈ λ, S * ⊑R, Trans(S) and R ∈ r i for some 1 ≤ i ≤ d σ + 1 then ∀S.D ∈ l i ; 11. If (≥ nS.C) ∈ λ then there are 1 ≤ i 1 < • • • < i n ≤ d σ + 1 such that C ∈ l ij and S ∈ r ij for all 1 ≤ j ≤ n; 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;
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 which satisfy λ σ and have R-neighbours such that R is included in their rays. Moreover, we can merge nodes satisfying homomorph and isomorph star-types without violating semantic constraints imposed by node and edge labels. A star-type σ is valid if no expansion rule is applicable to a node whose label is λ σ . Definition 7 (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, δ is a function δ : -If Φ(σ) is homomorph w.r.t. a star-type σ 0 ∈ Φ(σ) and r ′ , l ′ is a primary ray of σ 0 then we define a primary ray r, l of Φ(σ) with r = r ′ and l = l ′ ; -If Φ(σ) is isomorph and r ′ , l ′ is a primary ray of some fixed star-type σ 0 ∈ Φ(σ) then we define a primary ray r, l of Φ(σ) with r = r ′ and l = l ′ ; -If r ′ , l ′ is a non primary ray of Φ(σ) then there is some σ ′ ∈ Φ(σ) that has a non primary ray r, l such that r = r ′ and l = l ′ .

i∈{1,••• ,H} N i → N, Φ is a function Φ : i∈{1,••• ,H} N i → 2 i∈{1,••• ,H} Ni , and δ is a function δ ′ : Φ( i∈{1,••• ,H} N i ) → N; 1. Two star-types σ, σ ′ ∈ i∈{1,••• ,H} N i are mergeable in F, denoted σ ≈ σ ′ ,
We denote C Φ(σ) for the set of all rays of Φ(σ), and C

Φ(σ) ≤mR.C = { r ′ , l ′ ∈ C Φ(σ) | R ∈ r, C ∈ l}. 2. A star-type σ ∈ N k (0 ≤ k ≤ H) is called linkable with a star-type σ ′ ∈ N k-1 ∪
N k+1 by a ray r, l of σ if σ ′ has a ray r ′ , l ′ such that l = λ σ ′ , l ′ = λ σ and r = r ′-where r ′-= {R ⊖ | R ∈ r ′ }.

The frame structure, as introduced in Definition 7, allows us to tile star-types to obtain a forest structure. Such a structure is crucial to obtain termination when designing a tableaux-based algorithm. An important difference between a frame and a SHOIQforest is that a frame does not represent nodes corresponding to individuals but store the number of individuals satisfying a star-type. The function δ(σ) is used for this purpose. According to Lemma 1, the number of a SHOIQ-forest's nodes may be double exponential in the size of a SHOIQ knowledge base (T , R) while the number of distinct star-types is bounded by an exponential function since star-types are built from the signature of (T , R). This implies that δ(σ) may take a double exponential value. In the context of a SHOIQ-forest, we can think of a Φ(σ) as the set of partitions each of which satisfies all σ ′ ∈ Φ(σ). The function δ(σ) is used to store the number of partitions satisfying all σ ′ ∈ Φ(σ).

Definition 8 (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 σ ∈ i∈{1,••• ,H} N i , if δ(σ) ≥ 1 then σ is valid; 2. For each o ∈ C o there is a unique σ o ∈ N 0 such that o ∈ λ σo and δ(σ o ) = 1; 3. For each o ∈ C o , Φ(σ o ) = {σ ∈ i∈{1,••• ,H} N i | o ∈ λ σ } and δ(Φ(σ o )) = 1; 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 -,λ (1)
where |ν ω | λ,r,λ ′ and |μ ω | λ,r,λ ′ are denoted for the number of components r ′ , l ′ of respective νω and μω such that λ ω = λ, r ′ = r and l ′ = λ ′ for a star-type

ω = λ ω , νω , μω ; 5. For each λ, r, λ ′ ∈ 2 cl(T ,R) × 2 R (T ,R) × 2 cl(T ,R) with r -= {R ⊖ | R ∈ r}, Φ(σ) δ(Φ(σ))|Φ(σ)| λ,r,λ ′ = Φ(σ ′ ) δ(Φ(σ ′ ))|Φ(σ ′ ))| λ ′ ,r -,λ (2)
where |Φ(ω)| l,s,l ′ is denoted for the number of rays u, h of Φ(ω) with some star-type ω such that λ ω = l, u = s and h = l ′ . 6. For each Φ(σ) with σ ∈ i∈{1,••• ,H} N i , and for each term

(≤ mR.C) ∈ λ σ , card{C Φ(σ) ≤mR.C } ≤ m (3)
The notion of validity for a frame is crucial to establish a connection with the tableaux-based algorithm presented in Section 3, i.e., how to build a SHOIQ-forest from a valid frame, and inversely. Condition 1 in Definition 8 requires that every startype counted by δ must be valid. Condition 2 and 3 ensure that each nominal is counted exactly once. In the context of a SHOIQ-forest, these conditions imply that for each nominal o there is exactly one tree whose root contains o and there is exactly one partition contains o. 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 star-types at level k -1 and k + 1. The number of these neighbours corresponds exactly to the number of x's rays. Condition 5 guarantees that each partition satisfying Φ(σ) can be linked exactly with another partition via a ray of Φ(σ). Finally, Condition 5 ensures that each partition satisfying Φ(σ) with (≤ mR.C) ∈ λ σ can be linked at most with m partitions containing C via rays that include R. Lemma 2. Let (T , R) be a SHOIQ knowledge base.

If the tableaux algorithm can build a clash-free and complete SHOIQ-forest for

(T , R) then there is a valid frame for (T , R). δ,Φ,δ for (T ,R) then the tableaux algorithm can build a clash-free and complete SHOIQ-forest for (T , R).

If there is a valid frame

F = (N 0 , • • • , N H ),
Lemma 2 points out the equivalence between a clash-free and complete SHOIQforest and a valid frame for (T , R). The following lemma affirms that there is an exponential structure, a valid frame, which can represent a SHOIQ-forest whose size may be double exponential. Lemma 3. 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).

We can sketch a proof of the lemma here. We have

H ≤ K where K = 2 2m+k × 2 with m = card{cl(T , R)} and k = card{R (T ,R) }. card{Σ} ≤ (card{cl(T , R)}) 2 × card{R (T ,R) } δ(σ) ≤ M 2 2m+k ×2
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 for σ ∈ Σ. If δ(σ) is represented as a binary number then it takes an exponential number of bits.

Based on Lemma 3 and 2, we can present straightforwardly an optimal worst-case algorithm for checking the consistency of a SHOIQ knowledge base. However, such an algorithm cannot be used in practice since there are tremendously non-determinisms which must be dealt with when constructing a valid frame. In the sequel, based on the results obtained so far, we try to design an algorithm which has more goal-directed behaviours.

Blocking condition for a frame

Let F = (N 0 , • • • , N H ), δ, Φ, δ be a frame. A star- type σ k ∈ N k with 0 < k ≤ H is blocked if there are σ i ∈ N i with 0 ≤ i ≤ k such that σ i is linkable with σ i-1 for all i ∈ {1, • • • , k}, then there are 0 < k 1 < k 2 < k 3 < k 4 ≤ k such that: 1. λ σ k 1 = λ σ k 2 , νσ k 1 = νσ k 2 , and there is no 0 < j < k 2 such that j = k 1 , λ σj = λ σ k 2 and νσj = νσ k 2 ; 2. λ σ k 3 = λ σ k 4 , νσ k 3 = νσ k 4 ,
and there is no k 2 < j < k 4 such that j = k 3 , λ σj = λ σ k 4 and νσj = νσ k 4 . Notice that this blocking condition is looser than the blocking condition introduced in Definition 5 for a SHOIQ-forest. Since we can not determine the path from root to a node satisfying a star-type over a frame, it not possible to check blocking condition in the same way as for a SHOIQ-forest. The blocking condition for a frame, as described above, implies that a node satisfying a blocked star-type must have an ancestor which is blocked according to the blocking condition for a SHOIQ-forest.

We are now ready to propose an EXPSPACE tableaux-based algorithm for SHOIQ. Before applying the frame rules described in Figure 3 (Appendix), we initialise a frame F = (N 0 , • • • , N H ), δ, Φ, δ from a (T , R) knowledge base as follows:

N 0 := { {o}, ∅, ∅ | o ∈ C o }; δ(σ o ) := 1, Φ(σ o ) = {σ o } and δ ′ (Φ(σ o )) = 1 for all σ o ∈ N 0 .
If no frame rule is applicable to all star-types of F then we say that F is complete. If we obtain a valid and complete F by applying the frame rules from a (T , R), then we conclude that (T , R) is consistent. Otherwise, (T , R) is not consistent.

Soundness of the tableaux-based algorithm for building a frame can be established thanks to Lemma 2. Since each frame rule has its counterpart in the expansion rules, completeness of the algorithm can be shown by using the same arguments as those employed to prove Lemma 1. From these results and Lemma 3, we obtain the following main result of the section: Theorem 2. Let (T , R) be a SHOIQ knowledge base. The tableaux algorithm for contructing a frame is a decision procedure for consistency of (T , R) and it runs in EXPSPACE in the size of (T , R).

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 without adding nominal nodes with new nominals. This technique is founded on the fact that fusions of nodes triggered by merging nominal nodes can be replaced with governing a partitioning function which would simulate this merging process. This allows us to reuse the 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.

The algorithms proposed in the present paper have used several nondeterministic rules, e.g., ⊲⊳ or ≤ o -rules. We think that these rules should be improved in some way such that, for instance, they would take advantage of information from the part of the frame which has already built.

⊑-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 C1 ⊓ C2 ∈ L(x) and {C1, C2} ⊆ L(x) then L(x ′ ) = L(x ′ ) ∪ {C1, C2} for all x ′ ∈ ϕ(x). ⊔-rule: if C1 ⊔ C2 ∈ (x) and {C1, C2} ∩ L(x) = ∅ then L(x ′ ) = Lo(x ′ ) ∪ {C} with some C ∈ {C1, C2} for all x ′ ∈ ϕ(x). ∃-rule: if 1. ∃S.C ∈ L(x),
x is not blocked, x is not non-root nominal, and 2.

x has no S-neighbour y with C ∈ L(y) then create a new node y with L( x, y )={S}, L(y)={C} and ϕ(y) = {y}. ∀-rule: if 1. ∀S.C ∈ L(x), and 2. there is a S-neighbour y of x such that C / ∈ L(y) then L(y ′ ) = L(y ′ ) ∪ {C} for all y ′ ∈ ϕ(y). ∀+-rule: if 1. ∀S.C ∈ L(x), and 2. there is some Q with Trans(Q) and Q * ⊑S, and 3. there is an Q-neighbour y of x such that ∀Q.C / ∈ L(y) then L(y ′ ) = L(y ′ ) ∪ {∀Q.C} for all y ′ ∈ ϕ(y). ch-rule: if 1. (≤ n S.C) ∈ L(x), and 2. there is an S-neighbour y of x with {C, ¬C} ∩ L(y) = ∅ then L(y ′ ) = Lo(y ′ ) ∪ {E} with some E ∈ {C, ¬C} for all y ′ ∈ ϕ(y). ≥-rule: if 1. (≥ n S.C) ∈ L(x), x is not blocked, x is not non-root nominal, and 2.

x has no n S-neighbours y1, ..., yn such that C ∈ L(yi), and yi • =yj for 1 ≤ i < j ≤ n, then create n new nodes y1, ..., yn with L( x, yi )={S}, L(yi)={C}, ϕ(yi) = {yi} and yi • =yj 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).

Fig. 1. Expansion rules for SHIQ oϕ-rule: 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 y0,

• • • , yn with ϕ(yi) ∩ ϕ(yj) = ∅, 0 ≤ i < j ≤ n, C ∈ Λ(ϕ(yi)), R ∈ Λ( ϕ(x), ϕ(yi)
) for all 0 ≤ i ≤ n, and 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 ′′ ). then updateLabel(σ, λσ ∪ {C}) with some C ∈ {C1, C2}. ∃-rule: if 1. ∃S.C ∈ λσ, λσ is not blocked, and 2. σ has no ray r, l with S ∈ r and C ∈ l then addRay(σ, r, l). ∀-rule: if 1. ∀S.C ∈ λσ, and 2. σ has a ray r, l such that S ∈ r and C / ∈ l then if r, l ∈ νσ then updatePredRay(σ, r, l , r, l ∪ {C}) else updateSuccRay(σ, r, l , r, l ∪ {C}) ∀+-rule: if 1. ∀S.C ∈ λσ, and 2. there is some Q with Trans(Q) and Q * ⊑S, and 3. σ has a ray r, l such that Q ∈ r and ∀Q.C / ∈ l then if r, l ∈ νσ then updatePredRay(σ, r, l , r, l ∪ {∀Q.C}).

else updateSuccRay(σ, r, l , r, l ∪ {∀Q.C}) ch-rule: if 1. (≤ n S.C) ∈ λσ, and 2. σ has a ray r, l such that S ∈ r and {C, ¬C} ∩ l = ∅ then if r, l ∈ νσ then updatePredRay(σ, r, l , r, l ∪ {E}).

else updateSuccRay(σ, r, l , r, l ∪ {E}) with some E ∈ {C, ¬C}. ≥-rule: if 1. (≥ n S.C) ∈ λσ, σ is not blocked, and 2. σ has no n rays r1, l1 , ..., rn, ln such that R ∈ ri, C ∈ li, and ri, lj • = rj, lj for 1 ≤ i < j ≤ n, then call addRay(σ, {R}, {C}) n times to create n rays r1, l1 , ..., rn, ln with ri = {R} and li = {C} for 1 ≤ i ≤ n, and ri, li • = rj, lj for 1 ≤ i < j ≤ n. ≤-rule: if 1. (≤ n S.C) ∈ σ, and 2. σ has (n + 1) rays r0, l0 , ..., rn, ln such that R ∈ ri, C ∈ li for all 0 ≤ i ≤ n and there are 0 ≤ i < j ≤ n such that ri, li • = rj, lj does not hold then 1. For each r, l ∈ { ri, li , rj, lj }, if r, l ∈ νσ, then, updatePredRay(ω, r, l , r ∪ r ′ , l ∪ l ′ ), else, updateSuccRay(ω, r, l , r ∪ r ′ , l ∪ l ′ ) where r ′ , l ′ ∈ { ri, li , rj, lj } with r ′ , l ′ = r, l . 2. add r ′ , l ′ • = ri, li for all ray r ′ , l ′ such that r ′ , l ′ • = rj, lj . o-rule: if 1. there are star-types σ1,

• • • , σ k such that o ∈ λσ i for some o ∈ Co then updateLabel(σ1, • • • , σ k ), ≤o-rule: if 1. there are star-types σ1, • • • , σ k ∈ Φ(σ) and (≤ mR.C)} ∈ λσ i for all 1 ≤ i ≤ k, and σ1, • • • , σ k have (m + 1) distinct primary rays r0, l0 , • • • rm, lm such that R ∈ ri and C ∈ li for all 0 ≤ i ≤ m then 1. Choose two rays rj, lj , r j ′ , l j ′ of respective σi ∈ N h and σ i ′ ∈ N h ′ with 0 ≤ j < j ′ ≤ m and 1 ≤ i < i ′ ≤ k such that rj, lj • = r j ′ , l j ′ 2. For each r, l ∈ { rj, lj , r j ′ , l j ′ }, if r, l ∈ νω with ω ∈ {σi, σ i ′ }, then, updatePredRay(ω, r, l , r ∪ r ′ , l ∪ l ′ ), else, updateSuccRay(ω, r, l , r ∪ r ′ , l ∪ l ′ ) where r ′ , l ′ ∈ { rj, lj , r j ′ , l j ′ } with r ′ , l ′ = r, l . ⊲⊳-rule: if 1. (≤ nR.C) ∈ λσ, {(≤ l R.C), (≥ l R.C)} λσ for all l ≤ n, 2. (≤ k R.C) /
∈ λσ for all k < n, and 3. σ has a ray r, l such that R ∈ r, C ∈ l then 1. guess m with 1 ≤ m ≤ n, and 2. updateLabel(σ, λσ ∪ {≤ mR.C, ≥ mR.C}). Build a star-type ω with λω = λ σ ′ , νω = νσ ′ and μω := (μ σ ′ , r -, l0 );

4 N k-1 := N k-1 ∪ {ω}; 5 if σ ′ = ω0 then 6 δ(ω) := δ(σ) - ω ′ ∈N ′ (σ) δ(ω ′ ); 7 δ(σ ′ ) := δ(σ ′ ) -(δ(σ) - ω ′ ∈N ′ (σ)
δ(ω ′ )); 15

Let μσ = ( r1, l1 , • • • , ri, lj , • • • , r k ′ , l k ′ ); 16 foreach ri, li with 1 ≤ i ≤ k ′ do 17 Let N (σ, ri, li ) = N ′ (σ, ri, li ) ∪ {ω0}; 18 foreach σ ′ ∈ N (σ, ri, li ) do 19
Build a star-type ω with λω = li, νω = { r - i , l0 } and μω = μσ ′ ; 20 N k+1 := N k+1 ∪ {ω}; 39 Algorithm 4: updateSuccRay(σ, r, l , r 0 , l 0 ) updates frame when modifying a ray r, l / ∈ νσ of a star-type σ ∈ N k by assigning r 0 , l 0 to respective r and l.

21 if σ ′ = ω0 then 22 δ(ω) := δ(σ ′ ) - ω ′ ∈ N (σ, r i ,l i ) δ(ω ′ ); 23 δ(σ ′ ) := δ(σ ′ ) -(δ(σ) - ω ′ ∈ N (σ, r i ,l i ) δ(ω ′ ));

  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 ⊤

Fig. 2 . 2 N 7 else 8 N 20 Algorithm 1 :

 2278201 Fig. 2. New expansion rules for SHOIQ

Fig. 3 . 1 Let

 31 Fig. 3. Expansion rules for constructing a frame.

8 else 9 δ

 89 (ω) := δ(σ ′ ), δ(σ ′ ) := 0; 10 if ω ≈ ω ′ for all ω ′ ∈ i∈{1,••• ,H} Ni then11 Φ(ω) := {ω}, δ(Φ(ω)) := 1 and δ(Φ(σ ′ )) := δ(Φ(σ ′ )) -1; ∈ λω for all o ∈ Co then 14 δ(Φ(ω)) := δ(Φ(ω)) + 1;

7 N 8 if σ ′′ = ω ′ 0 then 9 δ 12 δ 9 N

 789129 ) := δ(σ ′ ), δ(σ ′ ) := 0; 26 if ω ≈ ω ′ for all ω ′ ∈ i∈{1,••• ,H} Ni then 27 Φ(ω) := {ω}, δ(Φ(ω)) := 1 and δ(Φ(σ ′ )) := δ(Φ(σ ′ )) -1; ∈ λω for all o ∈ Co then 30 δ(Φ(ω)) := δ(Φ(ω)) + 1; 31 Build a star-type ω with λω = l0, νω = νσ and μω = μσ; 32 δ(ω) := δ(σ), δ(σ) := 0, N k := N k ∪ {ω}; 33 if ω ≈ ω ′ for all ω ′ ∈ i∈{1,••• ,H} Ni then 34 Φ(ω) := {ω}, δ(Φ(ω)) := 1 and δ(Φ(σ ′ )) := δ(Φ(σ ′ )) -1; ∈ λω for all o ∈ Co then 37 δ(Φ(ω)) := δ(Φ(ω)) + 1; 38 Algorithm 2: updateLabel(σ, l 0 ) updates frame when modifying λ σ by assigning l to λ σ .Input : σ = λσ, μσ, νσ ∈ N k ; νσ = { r, l } r0 ⊆ R (T ,R) ; l0 ⊆ cl(T , R) and F = (N0, • • • , NH ), δ, Φ, δ Output: the frame obtained by updating F Let N (σ) = N ′ (σ) ∪ {ω0}; 1 foreach σ ′ ∈ N (σ) do 2 Let ν(σ ′ ) = { s, h }; 3 Let μ(σ ′ ) = ( s1, h1 , • • • , si, hi , • • • , sn, hn ) with si = r -and hi = λσ; 4 Let N (σ ′ ) = N ′ (σ ′ ) ∪ {ω ′ 0 }; 5 foreach σ ′′ ∈ N (σ ′ ) do 6Build a star-type ω with λω = λ σ ′′ , νω = νσ ′′ and μω = (μ σ ′′ , s -, λ σ ′ ); k-2 := N k-2 ∪ {ω}; (ω) := δ(σ ′ )ω ′ ∈N ′ (σ ′ ) δ(ω ′ ); 10 δ(σ ′′ ) := δ(σ ′′ ) -(δ(σ ′ )ω ′ ∈N ′ (σ ′ ) δ(ω ′ )); 11 else (ω) := δ(σ ′′ ), δ(σ ′′ ) := 0; 13 if ω ≈ ω ′ for all ω ′ ∈ i∈{1,••• ,H} Ni then 14 Φ(ω) := {ω}, δ(Φ(ω)) := 1 and δ(Φ(σ ′′ )) := δ(Φ(σ ′′ )) -1; ∈ λω for all o ∈ Co then 17 δ(Φ(ω)) := δ(Φ(ω)) + 1;18 Build a star-type ω with λω = l0, νω = νσ ′ and μω = (μ σ ′ , r - 0 , l0 );19 N k-1 := N k-1 ∪ {ω}; 20 if σ ′ = ω0 then 21 δ(ω) := δ(σ)ω ′ ∈N ′ (σ) δ(ω ′ ); 22 δ(σ ′ ) := δ(σ ′ ) -(δ(σ)ω ′ ∈N ′ (σ) δ(ω ′ ));23 else 24 δ(ω) := δ(σ ′ ), δ(σ ′ ) := 0; 25 if ω ≈ ω ′ for all ω ′ ∈ i∈{1,••• ,H} Ni then 26 Φ(ω) := {ω}, δ(Φ(ω)) := 1 and δ(Φ(σ ′ )) := δ(Φ(σ ′ )) -1; ∈ λω for all o ∈ Co then 29 δ(Φ(ω)) := δ(Φ(ω)) + 1; 30 Build a star-type ω with λω = λσ, νσ 0 = { r0, l0 } and μω = μσ; 31 δ(ω) := δ(σ), δ(σ) := 0, N k := N k ∪ {ω}; 32 if ω ≈ ω ′ for all ω ′ ∈ i∈{1,••• ,H} Ni then 33 Φ(ω) := {ω}, δ(Φ(ω)) := 1 and δ(Φ(σ)) := δ(Φ(σ)) -1; ∈ λω for all o ∈ Co then 36 δ(Φ(ω)) := δ(Φ(ω)) + 1;37 Algorithm 3: updatePredRay(σ, r, l , r 0 , l 0 ) updates frame when modifying a ray r, l of a star-type σ ∈ N k by assigning r 0 , l 0 to respective r and l.Input : σ = λσ, μσ, νσ ∈ N k ; r, l / ∈ νσ is ray of σ; r0 ⊆ R (T ,R) ; l0 ⊆ cl(T , R)and F = (N0, • • • , NH ), δ, Φ, δ Output: the frame obtained by updating FLet μσ = ( r1, l1 , • • • , ri, li , • • • , r k , l k ); 1 foreach ri, li with 1 ≤ i ≤ k do 2 Let N (σ, ri, li ) = N ′ (σ, ri, li ) ∪ {ω0}; 3 foreach σ ′ ∈ N (σ, ri, li ) do 4 Let μσ ′ = ( s1, h1 , • • • , sj, hj , • • • , s k ′ , h k ′ ); 5 foreach sj, hj with 1 ≤ j ≤ k ′ do 6 Let N (σ ′ , sj, hj ) = N ′ (σ ′ , sj, hj ) ∪ {ω1}; 7 foreach σ ′′ ∈ N (σ ′ , sj, hj ) do 8Build a star-type ω with λω = hj, νω = { s - j , λ σ ′ } and μω = μσ ′′ ; k+2 := N k+2 ∪ {ω};10 if σ ′′ = ω1 then 11 δ(ω) := δ(σ ′ )ω ′ ∈ N (σ ′ , s j ,h j ) δ(ω ′ ); 12 δ(σ ′′ ) := δ(σ ′′ ) -(δ(σ ′ )ω ′ ∈ N (σ ′ , s j ,h j ) δ(ω ′ )); ) := δ(σ ′′ ), δ(σ ′′ ) := 0; 15 if ω ≈ ω ′ for all ω ′ ∈ i∈{1,••• ,H} Ni then 16 Φ(ω) := {ω}, δ(Φ(ω)) := 1 and δ(Φ(σ ′′ )) := δ(Φ(σ ′′ )) -1; ∈ λω for all o ∈ Co then 19 δ(Φ(ω)) := δ(Φ(ω)) + 1; 20 Build a star-type ω with λω = li, νω = { r - i , λσ } and μω = μσ ′ ; 21 N k+1 := N k+1 ∪ {ω};22 if σ ′ = ω0 then 23 δ(ω) := δ(σ)ω ′ ∈ N (σ, r i ,l i ) δ(ω ′ ); 24 δ(σ ′ ) := δ(σ ′ ) -(δ(σ)ω ′ ∈ N (σ, r i ,l i ) δ(ω ′ )); 25 else 26 δ(ω) := δ(σ ′ ), δ(σ ′ ) := 0; 27 if ω ≈ ω ′ for all ω ′ ∈ i∈{1,••• ,H} Ni then 28 Φ(ω) := {ω}, δ(Φ(ω)) := 1 and δ(Φ(σ ′ )) := δ(Φ(σ ′ )) -1; ∈ λω for all o ∈ Co then 31 δ(Φ(ω)) := δ(Φ(ω)) + 1; 32 Build a star-type ω with λω = l0, νω = νσ and μω = (μσ, r0, l0 ); 33 δ(ω) := δ(σ), δ(σ) := 0, N k := N k ∪ {ω}; 34 if ω ≈ ω ′ for all ω ′ ∈ i∈{1,••• ,H} Ni then 35 Φ(ω) := {ω}, δ(Φ(ω)) := 1 and δ(Φ(σ)) := δ(Φ(σ)) -1; 36 else 37 if o / ∈ λω for all o ∈ Co then 38 δ(Φ(ω)) := δ(Φ(ω)) + 1;

  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

  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

  if, either σ and σ ′ are homomorph to a star-type σ 0 ; or σ and σ ′ are isomorph. The relation of mergeability ≈ is an equivalence relation over i∈{1,••• ,H} N i . We denote Φ(σ) = {σ ′ | σ ′ ≈ σ} and Φ(σ) is called mergeable. We say that Φ(σ) is homomorph w.r.t. a star-type σ 0 if σ ′ is homomorph to σ 0 for all σ ′ ∈ Φ(σ). We say that Φ(σ) is isomorph if σ ′ , σ ′′ are isomorph for all σ ′ , σ

′′

∈ Φ(σ). For each Φ(σ), we define a set of rays of Φ(σ) as follows:

Appendix

The rules in Figure 3 for building a frame calls the algorithms described in Figure 1, 2, 3 and 4. Basically, these algorithms update the frame by adding a new star-type or modifying the functions δσ and δσ.

, and for all σ ′ ∈ N (σ) it holds that λ σ ′ = l 0 , σ ′ has a ray r ′′ , l ′′ / ∈ νσ ′ with r ′′ = r - 0 and l ′′ = λ σ . -For each ray r, h of σ with r, h / ∈ νσ , we denote N (σ, e, h ) ⊆ N k+1 for the non-empty set with N (σ, e, h ) = N ′ (σ, e, h ) ∪ {ω 0 } such that

, and for all σ ′ ∈ N (σ, e, h ) it holds that λ σ ′ = h, σ ′ has a ray r ′′ , l ′′ ∈ νσ ′ with r ′′ = r -and l ′′ = λ σ .