=Paper=
{{Paper
|id=None
|storemode=property
|title=An ExpSpace Tableau-based Algorithm for SHOIQ
|pdfUrl=https://ceur-ws.org/Vol-846/paper_51.pdf
|volume=Vol-846
|dblpUrl=https://dblp.org/rec/conf/dlog/DucLC12
}}
==An ExpSpace Tableau-based Algorithm for SHOIQ==
https://ceur-ws.org/Vol-846/paper_51.pdf
An E XP S PACE Tableau-based Algorithm for SHOIQ
Chan Le Duc1 , Myriam Lamolle1 , and Olivier Curé2
1
LIASD Université Paris 8 - IUT de Montreuil, France
{chan.leduc, myriam.lamolle}@iut.univ-paris8.fr
2
LIGM Université Paris-Est, France
ocure@univ-mlv.fr
Abstract. In this paper, we propose an E XP S PACE tableau-based algorithm for
SHOIQ. The construction of this algorithm is founded on the standard tableau-
based method for SHOIQ and the technique used for designing a NE XP T IME
algorithm for the two-variable fragment of first-order logic with counting quanti-
fiers C 2 .
1 Introduction
The ontology language OWL-DL [6] 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 [9]. There have been 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. Tobies [9] has shown that the consistency
problem of a SHOIQ knowledge base is N EXP T IME-complete. Horrocks et al. [2]
have proposed a tableau-based algorithm that has been exploited to implement reasoners
such as Pellet [8], which inherit from the success of early Description Logic reasoners
such as FaCT [1].
It has been shown that when nominals are added to DLs the consistency problem is
harder. In fact, the complexity jumps from E XP T IME-complete for SHIQ to N EXP -
T IME-complete for SHOIQ [9]. Kazakov et al. [4] have indicated that when nominals
are allowed in SHIQ, the resolution-based approach yields a triple exponential deci-
sion 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 the technique that was employed by Pratt-Hartmann
[7] to construct a NE XP T IME algorithm for the logic C 2 that almost includes SHOIQ.
Unlike the existing tableau-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. Pratt-Hartmann [7] 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 de-
scribes a 2E XP S PACE tableau-based algorithm for checking consistency of a SHOIQ
knowledge base. An advantage of this algorithm is that a tree-like structure can be main-
tained to obtain termination. Section 4 transfers results from C 2 [7] to SHOIQ, and
presents an E XP S PACE tableau-based algorithm for SHOIQ. Finally, we discuss the
results and future work. For the lack of place, we refer the reader to [5] for examples
and full proofs.
2 The Description Logic SHOIQ
In this section, we present the syntax and the semantics of SHOIQ. We start by defin-
ing 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 RI = {P − | P ∈ R} to denote a set of inverse
roles. Each element of R∪RI is called a SHOIQ-role. We define R := R− if R ∈ R,
and R := R if R ∈ RI . A role hierarchy R is a finite set of role inclusion axioms
R v S where R and S are two SHOIQ-roles. A relation v ∗ is defined as the transitive-
reflexive closure of v on R∪{R v S | R v S ∈ R}. We define a function Trans(R)
which returns true iff there is some Q ∈ R+ ∪ {P | P ∈ R+ } such that QvR. ∗ A
role R is called simple w.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
I
to a subset of ∆I × ∆I such that R− = {hx, yi ∈ ∆I × ∆I | hy, xi ∈ RI } for
all R ∈ R, and hx, zi ∈ S , hz, yi ∈ S I implies hx, yi ∈ S I for each S ∈ R+ . An
I
interpretation I satisfies a role hierarchy R if RI ⊆ S I for each R v S ∈ R. Such an
interpretation is called a model of R, denoted by I |= R.
Definition 2 (terminology). Let C be a non-empty set of concept names with a non-
empty subset Co ⊆ C of nominals. The set of SHOIQ-concepts is inductively defined
as the smallest set containing all C in C, >, CuD, CtD, ¬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 u D)I = C I ∩ DI , (C t D)I = C I ∪ DI ,
(¬C)I = ∆I \C I , card{oI } = 1 for all o ∈ Co , (∃R.C)I = {x ∈ ∆I | ∃y ∈
∆I , hx, yi ∈ RI ∧ y ∈ C I }, (∀R.C)I = {x ∈ ∆I | ∀y ∈ ∆I , hx, yi ∈ RI ⇒
y ∈ C I }, (≥ n S.C)I = {x ∈ ∆I | card{y ∈ C I | hx, yi ∈ S I } ≥ n},
(≤ n S.C)I = {x ∈ ∆I | card{y ∈ C I | hx, yi ∈ S I } ≤ n}
where card{S} is denoted for the cardinality of a set S.
∗ C v D is called a general concept inclusion (GCI) where C, D are SHOIQ-
concepts (possibly complex), and a finite set of GCIs is called a terminology T .
∗ An interpretation I satisfies a GCI C v D if C I ⊆ DI 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 interpre-
tation I such that I |= R, I |= T and C I 6= ∅. 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 v D, if C I ⊆ DI holds in each model I of (T , R).
Thanks to the reductions between unsatisfiability, subsumption of concepts and knowl-
edge 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 [3]. 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 [2] 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 [2], we add a new property that imposes an exact
number of S-neighbour individuals t of s if (≤ nS.C) ∈ L(s). This property makes
explicit non-determinism implied from the semantics of (≤ nS.C) and requires an extra
expansion rule for the tableau-based algorithm.
3 A 2E XP S PACE 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 (tree). Let (T , R) be a SHOIQ knowledge base. For each o ∈ Co , a
·
SHOIQ-tree for (T , R), denoted by To = (Vo , Eo , Lo , x bo , 6= o ), is defined as follows:
∗ Vo is a set of nodes containing a root node x bo ∈ Vo . Each node x ∈ Vo is labelled
with a function Lo such that Lo (x) ⊆ cl(T , R) and o ∈ Lo (b xo ). A node x ∈ Vo is
called nominal if o0 ∈ Lo (x) for some o0 ∈ Co . In addition, the inequality relation 6= ·
o
is a symmetric binary relation over Vo .
∗ Eo is a set of edges. Each edge hx, yi ∈ Eo is labelled with a function Lo such that
Lo (hx, yi) ⊆ R(T ,R) . If hx, yi ∈ Eo then y is called a successor of x, denoted by
y ∈ succ1 (x), or x is called the predecessor of y, denoted by x = pred1 (y). In this
case, we say that x is a neighbour of y or y is a neighbour of x. If z ∈ succn (x)
(resp. z = predn (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 succ0 (x) = {x} and
pred0 (x) = x. A node y is called a descendant of x if y ∈ succn (x) for some n > 0.
A node y is called an ancestor of x if y = predn (x) for some n > 0. To ensure that
bo for all x ∈ Vo with x 6= x
To is a tree, it is required that (i) x is a descendant of x bo ,
and (ii) each node x ∈ Vo with x 6= x bo has a unique predecessor. A node y is called
an R-successor of x, denoted by y ∈ succ1R (x) (resp. y is called the R-predecessor
of x, denoted by y = pred1R (x)) if there is some role R0 such that R0 ∈ Lo (hx, yi)
(resp. R0 ∈ Lo (hy, xi)) and R0 vR. ∗ 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
(n+1)
R-predecessor of y) and y ∈ succnR (x) (resp. y = prednR (x)) then z ∈ succR (x)
(n+1) 0 0
(resp. z = predR (x)) for n ≥ 0 with succR (x) = {x} and x = predR (x).
∗ For a node x, a role S and o ∈ Co , we define the set S To (x, C) of x’s S-neighbours
as follows: S To (x, C) = {y ∈ Vo | y is a S-neighbour of x and C ∈ Lo (x)}.
∗ A node x is called iterated by y w.r.t. a node xo if x has no nominal ancestor except
bo and there are integers n, m > 0 and nodes x0 , y 0 such that : (i) xo = predn (y),
for x
y = predm (x), (ii) x0 = pred1 (x), y 0 = pred1 (y), (iii) Lo (x) = Lo (y), Lo (x0 ) =
Lo (y 0 ), (iv) Lo (hx0 , xi) = Lo (hy 0 , yi), and (v) if there are z, z 0 and i > 0 such that
z 0 = pred1 (z), predi (z 0 ) = xo , Lo (z) = Lo (y), Lo (z 0 ) = Lo (y 0 ) and Lo (hz 0 , zi) =
Lo (hy 0 , yi) then i ≥ n.
A node x is called 1-iterated by y if x is iterated by y w.r.t. x bo . 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 xo .
·
∗ In the following, we often use L(x), L(hx, yi), S T (x, C) and 6= instead of Lo (x),
To ·
Lo (hx, yi), S (x, C) and 6=o , respectively. This does not cause any confusion since
Vo ∩ Vo0 = ∅ and Eo ∩ Eo0 = ∅ if o 6= o0 . In addition, x6= ·
o y is never defined for x ∈ Vo
0
and y ∈ Vo0 with o 6= o .
We remark that the definition of 1-iterated nodes in Definition 4 for SHOIQ-trees
is very similar to the standard definition of blocked nodes for SHIQ completion trees
(see [3]). Moreover, if we consider the sub-tree 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 b(x), such that b
b(x) is an ancestor of x.
Definition 5 (forest). Let (T , R) be a SHOIQ knowledge base. A SHOIQ-forest
for (T , R) is a pair G = hT, ϕi, where T = {To | o ∈ Co } is a set of SHOIQ-
·
trees for (T , R) with
S To = (Vo , Eo , Lo , x
bo , 6= o ), and ϕ is a partitioning function ϕ :
V 0
V → 2 with V = o∈Co Vo . We denote L (hx, yi) = Lo (hx, yi) if hx, yi ∈ Eo , and
L0o (hx, yi) = {S | S ∈ Lo (hy, xi)} if hy, xi ∈ Eo for some o ∈ Co . The partitioning
function ϕ satisfies the following conditions:
1. For each x ∈ V, ϕ(x) is the partition of x with x ∈ ϕ(x). S There are x0 , · · · , xn ∈ V
such that ϕ(xi ) ∩ ϕ(xj ) = ∅ with 0 ≤ i < j ≤ n and 0≤i≤n ϕ(xi ) = V;
2. For all x, x0 ∈ V, if x0 ∈ ϕ(x) then ϕ(x) = ϕ(x0 ) and L(x) = L(x0 ). We de-
note Λ(ϕ(x)) = L(x). In addition, an inequality relation over partitions can be
described as follows : for x, x0 ∈ V we define ϕ(x)6= ·
ϕ(x0 ) if there are two nodes
0 0 · 0
y ∈ ϕ(x) and y ∈ ϕ(x ) such that y 6=o y for some o ∈ Co ;
3. For all ϕ(x) and ϕ(x0 ), if there are two edges hy, y 0 i ∈ Eo and hw, w0 i ∈ Eo0 with
o, o0 ∈ Co such that y, w ∈ ϕ(x), y 0 , w0 ∈ ϕ(x0 ), L0 (hy, y 0 i) 6= ∅, L0 (hw, w0 i) 6= ∅
then L0 (hy, y 0 i) = L0 (hw, w0 i).
We define a function Λ(h·, ·i) for labelling edges ended by two partitions as follows:
Λ(hϕ(x), ϕ(x0 )i) = L0 (hz, z 0 i) where z ∈ ϕ(x), z 0 ∈ ϕ(x0 ), L0 (hz, z 0 i) 6= ∅, and
{hz, z 0 i, hz 0 , zi} ∩ Eo0 6= ∅ for some o0 ∈ Co . We say ϕ(x0 ) is a S-neighbour
partition of ϕ(x) if S ∈ Λ(hϕ(x), ϕ(x0 )i).
4. For all x, x0 ∈ V, if o ∈ L(x) ∩ L(x0 ) for some o ∈ Co and ϕ(x)6= ·
ϕ(x0 ) does not
0
hold then ϕ(x) = ϕ(x );
5. If (≤ nR.C) ∈ Λ(ϕ(x)) for some x ∈ V and there exist (n+1) nodes x0 , · · · , xn ∈
V such that (i) ϕ(xi ) ∩ ϕ(xj ) = ∅ for all 0 ≤ i < j ≤ n, and (ii) C ∈ Λ(ϕ(xi )),
·
R ∈ Λ(hϕ(x), ϕ(xi )i) for all i ∈ {0, · · · , n}, then ϕ(xl )6= ϕ(xm ) for all 0 ≤ l <
m ≤ n; and
6. If (≥ nR.C) ∈ Λ(ϕ(x)) for some x ∈ V then ϕ(x) has n R-neighbour partitions
ϕ(x1 ), · · · , ϕ(xn ) such that ϕ(xi ) ∩ ϕ(xj ) = ∅ and C ∈ Λ(ϕ(xi )) 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)6= ϕ(y) and o ∈ Λ(ϕ(x)) ∩ Λ(ϕ(y)) for
some o ∈ Co ;
3. There is a node x ∈ V with (≤ nR.C) ∈ Λ(ϕ(x)) and there are (n + 1) nodes
·
x0 , · · · , xn ∈ V such that ϕ(xi ) ∩ ϕ(xj ) = ∅, ϕ(xi )6= ϕ(xj ) with 0 ≤ i < j ≤ n,
and C ∈ Λ(ϕ(xi )), R ∈ Λ(hϕ(x), ϕ(xi )i) for i ∈ {0, · · · , n}.
We now describe the tableau-based algorithm whose goal is to construct from a
knowledge base (T , R) a SHOIQ-forest G = hT, ϕi. To do this, the algorithm ap-
plies expansion rules (as described in Fig. 1 and Fig. 2 in [5]), 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 To is complete and clash-free
for all To ∈ T.
The expansion rules maintain the tree-like structure of SHOIQ-forest and they are
similar to those in [2] 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 Fig. 1 in [5] except for ∃- and ≥-rule update only the label of
nodes or edges and do not change the partitioning function ϕ. In particular, when the
≤-rule is applied to a node x with two S-neighbours y, z of x, it must propagate the
label of hx, yi to that of all hx0 , z 0 i (or hz 0 , x0 i) where x0 ∈ ϕ(x) and z 0 ∈ ϕ(z), and
set the label of hx, yi to empty set. This may change ϕ only if ϕ(y) is singleton. By a
new rule, namely the ./-rule, 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 0 ∈ ϕ(x) then y and y 0 have exactly m S-neighbours
which contain C in their label. Finally, we can avoid infinite sequences of “merging-
and-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 tableau algorithm terminates and builds a SHOIQ-forest whose the size is
bounded by a doubly exponential function in the size of (T , R).
2. If the tableau 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 tableau algorithm yields a clash-free and
complete SHOIQ-forest for (T , R).
To prove soundness of the tableau algorithm, we can devise a model from a clash-free
and complete SHOIQ-forest by considering a partition as an individual and unravel-
ling blocked nodes since we can show that each blocking node b(x) has no “core path”
from b(x) to each nominal descendant y, i.e., there do not exist terms (≤ mi Ri .Ci ) ∈
predi (y), roles Ri ∈ L(hpredi−1 (y), predi (y)i) and concepts Ci ∈ L(predi+1 (y)) for
k < i ≤ 0, b(x) = predk (y). The following theorem is a consequence of Lemma 1.
Theorem 1. Let (T , R) be a SHOIQ knowledge base. The tableau algorithm is a
decision procedure for consistency of (T , R) and it runs in 2NE XP T IME in the size of
(T , R).
4 An E XP S PACE Tableau-based Algorithm for SHOIQ
This section starts by translating some results presented in [7] 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 σ = hλσ , ν̄σ , µ̄σ i, where λσ ∈ 2cl(T ,R) , µ̄σ = (hr1 , l1 i, · · · , hrd , ld i) is a d-
tuple over 2R(T ,R) × 2cl(T ,R) , and ν̄σ = (hr0 , l0 i) with hr0 , l0 i ∈ 2R(T ,R) × 2cl(T ,R) .
A pair hr, li is a ray of σ if hr, li is a component of µ̄σ or ν̄σ . In particular, hr, li is a
predecessor ray if (hr, li) = ν̄σ , and hr, li is a successor ray if hr, li is a component
of µ̄σ . We denote ξ¯σ = (hr1 , l1 i, · · · , hrd , ld i, hrd+1 , ld+1 i) if ν̄σ = (hr0 , l0 i) where
r0 = rd+1 , l0 = ld+1 , and ξ¯σ = µ̄σ if ν̄σ is empty.
– A ray hr0 , l0 i of σ is primary w.r.t. a term (≤ mR.C) if (≤ mR.C) ∈ λσ , R ∈ r0
and C ∈ l0 . For a term (≤ mR.C) ∈ λσ , we denote Ch≤mR.Ci σ
for the set of all
0 0 0 0
rays hr , l i of σ such that R ∈ r , C ∈ l .
– A star-type σ is nominal if o ∈ λσ for some o ∈ Co .
– A star-type σ is chromatic if there is a term (≥ nS.D) ∈ λσ and σ has n rays
hr10 , l10 i, · · · , hrn0 , ln0 i such that S ∈ li0 , D ∈ li0 for all 1 ≤ i ≤ n, and li0 6= lj0 for all
0 ≤ i < j ≤ n with l00 = λσ .
– A star-type σ is homomorphic (resp. isomorphic) to a star-type σ 0 if λσ = λσ0 ,
and for each term (≤ mR.C) ∈ λσ , there is an injection (resp. a bijection) π :
σ0
σ
Ch≤mR.Ci → Ch≤mR.Ci such that π(hr, li) = hr0 , l0 i implies r0 = r and l0 = l.
– Two star-types σ, σ 0 are equivalent if λσ = λσ0 , and there is a bijection π between
ξ¯σ and ξ¯σ0 such that π(hr, li) = hr0 , l0 i implies r0 = r and l0 = l.
We denote Σ for the set of all star-types for (T , R). C
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 hri , li i of σ corresponds to a neighbour xi of x
such that L0 (hx, xi i) = ri and L(xi ) = li . In this case, we say that x satisfies σ.
Remark 1. The notion of chromaticity introduced in Definition 6 implies an inequality
·
relation 6= over nodes. That stronger notion is needed to prevent “distinct” star-types
·
from including nodes x, y which are neighbours or x6= 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.D) ∈
0 n
cl(T , R), we add to cl(T , R) n new concept names C(≥nS.D) , · · · , C(≥nS.D) , and to
i j
T the following axioms: C(≥nS.D) u C(≥nS.D) v ⊥ for all 0 ≤ i < j ≤ n. It is
straightforward to prove that the terminology (T 0 , R) is consistent iff (T , R) is con-
sistent where T 0 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 7 (valid star-type). Let (T , R) be a SHOIQ knowledge base. Let σ be
a star-type for (T , R) where σ = hλσ , ν̄, µ̄i with µ̄ = (hr1 , l1 i, · · · , hrd , ld i) and
·
λσ = l0 , ν̄ = {hrd+1 , ld+1 i}. σ is valid with an inequality relation 6= over C σ if the
following conditions are satisfied:
1. If C v D ∈ T then nnf(¬C t D) ∈ li for all 0 ≤ i ≤ d + 1;
2. {A, ¬A} 6⊆ li for every concept name A with 0 ≤ i ≤ d + 1;
3. If C1 u C2 ∈ li then {C1 , C2 } ⊆ li for all 0 ≤ i ≤ d + 1;
4. If C1 t C2 ∈ li then {C1 , C2 } ∩ li 6= ∅ for all 0 ≤ i ≤ d + 1;
5. If ∃R.C ∈ λσ then there is some 1 ≤ i ≤ d + 1 such that C ∈ li and R ∈ ri ;
6. If (≤ nS.C) ∈ λσ and there is some 1 ≤ i ≤ d + 1 such that S ∈ ri then C ∈ li
or ¬C
˙ ∈ li ;
7. If (≤ nS.C) ∈ λσ and there is some 1 ≤ i ≤ d + 1 such that C ∈ li and S ∈ ri
then there is some 1 ≤ m ≤ n such that {(≤ mS.C), (≥ mS.C)} ⊆ λ;
8. For each 1 ≤ i ≤ d + 1, if R ∈ ri and RvS ∗ then S ∈ ri ;
9. If ∀R.C ∈ λσ and R ∈ ri for some 1 ≤ i ≤ d + 1 then C ∈ li ;
10. If ∀R.D ∈ λσ , S vR,
∗ Trans(S) and R ∈ ri for some 1 ≤ i ≤ d+1 then ∀S.D ∈ li ;
0
11. If (≥ nS.C) ∈ λσ then C(≥nS.C) ∈ λσ and there are 1 ≤ i1 < · · · < in ≤ d + 1
j
such that {C, C(≥nS.C) } ⊆ lij , S ∈ rij for all 1 ≤ j ≤ n.
12. If (≤ nS.C) ∈ λσ and there are no 1 ≤ i1 < · · · < in+1 ≤ d + 1 such that C ∈ lij
and S ∈ rij for all 1 ≤ j ≤ n + 1. C
Notice that a valid star-type according to Definition 7 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 7, if
there is a term (≤ nS.D) ∈ λσ for a valid star-type σ then σ has exactly n primary rays
hri , li i, · · · , hrn , ln i w.r.t. (≤ nS.D).
Definition 8 (frame). Let (T , R) be a SHOIQ knowledge base. A frame for (T , R) is
a tuple F = h(N0 , · · · , NH ), δ, Φ, δi,
b where H ∈ N is the dimension of F; Ni ⊆ Σ for
S
all 0 ≤ i ≤ H, and all star-types in N0 are nominal. We denote N = i∈{1,··· ,H} Ni ;
δ is a function δ : N → N; Φ is a function Φ : N̄ → Σ where N̄ is denoted for the set of
all star-types σ ∈ N such that one of the three condition holds : (i) σ is nominal; (ii) σ
has a ray hr, li such that there is a term (≤ mR.C) with (≤ mR.C) ∈ λσ , C ∈ l and
R ∈ r; (iii)σ has a ray hr, li such that there is a term (≤ mR.C) with (≤ mR.C) ∈ l,
C ∈ λσ and R ∈ r; δb is a function δb : Φ(N̄) → N which is defined as follows:
For two star-types σ, σ 0 ∈ N̄, Φ(σ) = Φ(σ 0 ) iff either σ is isomorphic to σ 0 , or
there is a star-type ω ∈ N \ NH such that σ and σ 0 are homomorphic to ω.
Additionally, a star-type σ ∈ Nk (0 < k < H) is linkable with a star-type σ 0 ∈ Nk−1
by a ray hr, li of σ if σ 0 has a ray hr0 , l0 i such that λσ0 = l, r0 = r− and l0 = λσ where
r− = {R | R ∈ r}.
Remark 2. For σ, σ 0 ∈/ NH and σ, σ 0 are valid, if σ is homomorphic to σ 0 then σ is
isomorphic to σ . In fact, if there is a term (≤ mR.C) ∈ λσ then both σ, σ 0 have
0
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 8, 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. In the
context of a SHOIQ-forest, we can think of Φ(σ) as a star-type which is satisfied
by nodes forming a set of partitions. In fact, the function Φ maps star-types forming a
SHOIQ-forest into another set of star-types that regroups non-neighbour partitions.
Notice that the function Φ introduced in Definition 8 does not transfer the relation
of linkability from N̄ to Φ(N̄), and that chromaticity of star-types prevents chromati-
cally linkable star-types from collapsing into a unique star-type by the function Φ. The
function δ(Φ(σ))
b counts the number of partitions that are mapped to a star-type by Φ.
Such a function can be defined if all star-types “covering” a partition must be mapped
to a unique star-type by Φ. This is a consequence of the Φ’s definition.
Definition 9 (valid frame). Let (T , R) be a SHOIQ knowledge base. A frame F =
h(N0 , · · · , NH ), δ, Φ, δi
b is valid if the following conditions are satisfied:
1. For each σ ∈ N, if δ(σ) ≥ 1 then σ is valid;
2. For each σ ∈ N̄, if δ(σ) ≥ 1 then δ(Φ(σ))
b ≥ 1;
3. For each o ∈ Co there is a unique σo ∈ N0 such that o ∈ λσo and δ(σo ) = 1;
4. For each σ ∈ N, if o ∈ λσ with some o ∈ Co then Φ(σ) = Φ(σo ) and δ(Φ(σ b o )) =
1 with σo ∈ N0 such that o ∈ λσo and δ(σo ) = 1;
5. For each 0 ≤ k < H and hλ, r, λ0 i ∈ 2cl(T ,R) × 2R(T ,R) × 2cl(T ,R) with r− =
{R | R ∈ r},
X X
δ(σ)|µ̄σ |hλ,r,λ0 i = δ(σ 0 )|ν̄σ0 |hλ0 ,r− ,λi
σ∈Nk σ 0 ∈Nk+1
where |ν̄σ |hλ,r,λ0 i and |µ̄σ |hλ,r,λ0 i are denoted for the number of components hr0 , l0 i
of respective ν̄σ and µ̄σ such that λσ = λ, r0 = r and l0 = λ0 ;
6. For each hλ, r, λ0 i ∈ 2cl(T ,R) × 2R(T ,R) × 2cl(T ,R) with r− = {R | R ∈ r},
X X
δ(Φ(σ))
b ξ¯Φ(σ) hλ,r,λ0 i = δ(Φ(σ
b 0
)) ξ¯Φ(σ0 ) hλ0 ,r− ,λi
σ∈N̄ σ 0 ∈N̄
where ξ¯Φ(σ) hλ,r,λ0 i = ν̄Φ(σ) hλ,r,λ0 i + µ̄Φ(σ) hλ,r,λ0 i C
Remark 3. It is not required that star-types Φ(σ) are valid. We will use function Φ to
trim rays hr, li of star-types such that (i) hr, li or hr− , li is not a primary ray of every
star-type. The images of star-types σ by Φ, i.e. trimmed star-types Φ(σ), are employed
to represent partitions obtained from merge processes. As described in Section 3, in
order to govern partitions, it suffices to deal with nodes x containing a term (≤ mR.C)
and the R-neighbours of x containing C. For this reason, the function Φ maps only
star-types in N̄ by trimming non-primary rays.
The notion of validity for a frame is crucial to establish a connection with the
tableau-based algorithm presented in Section 3, i.e., how to build a SHOIQ-forest
from a valid frame, and inversely. The condition 1 in Definition 9 requires that every
star-type satisfied by at least one node must be valid. The condition 2 implies that each
valid star-type including a primary ray will be mapped by Φ. The condition 3 ensures
that each nominal is counted exactly once while the condition 4 imposes that all nomi-
nal star-types containing some o ∈ Co are mapped into a unique star-type by Φ. In the
context of a SHOIQ-forest, these conditions imply that for each nominal o ∈ Co there
is exactly one tree whose root contains o and there is exactly one partition containing
o. The condition 5 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 σ’s rays. Finally, the
condition 6 deals with partitions. In the context of a SHOIQ-forest where Φ(σ) rep-
resents the image of a set of partitions, the condition 6 points out how star-types Φ(σ)
would be interconnected.
Lemma 2. Let (T , R) be a SHOIQ knowledge base.
1. If the tableau algorithm can build a clash-free and complete SHOIQ-forest for
(T , R) then there is a valid frame for (T , R).
2. If there is a valid frame F = h(N0 , · · · , NH ), δ, Φ, δi
b for (T , R) then the tableau
algorithm can build a clash-free and complete SHOIQ-forest for (T , R).
Lemma 2 points out the equivalence between a clash-free and complete SHOIQ-
forest and a valid frame for (T , R). The following lemma affirms that there is an expo-
nential structure, a valid frame, which can represent a SHOIQ-forest whose size may
be doubly exponential.
Lemma 3. Let (T , R) be a SHOIQ knowledge base. The size of a valid frame F =
h(N0 , · · · , NH ), δ, Φ, δi
b 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 = 22m+k × 2
with m = card{cl(T , R)} and k P = card{R(T ,R) }. Moreover, each star-type has at
most M distinct rays where M = mi + E, mi occurs in a number restriction term
(≥ mi 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 δ(σ 0 ) where σ 0 , σ are respective star-
2m+k
×2
types at level k − 1 and k, it holds that δ(σ) ≤ M 2 . 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 the non-determinism is not sufficiently
constrained to obtain termination in feasible time. In the sequel, based on the results
obtained so far, we try to design an algorithm which has more goal-directed behaviour.
Blocking Condition for a Frame Let F = h(N0 , · · · , NH ), δ, Φ, δi b be a frame. A star-
type σk ∈ Nk with 0 < k ≤ H is blocked if there are σi ∈ Ni with 0 ≤ i ≤ k such
that σi is linkable with σi−1 for all i ∈ {1, · · · , k}, then there are 0 < k1 < k2 < k3 <
k4 ≤ k such that:
1. λσk1 = λσk2 , ν̄σk1 = ν̄σk2 , and there is no 0 < j < k2 such that j 6= k1 , λσj = λσk2
and ν̄σj = ν̄σk2 ;
2. λσk3 = λσk4 , ν̄σk3 = ν̄σk4 , and there is no k2 < j < k4 such that j 6= k3 ,
λσj = λσk4 and ν̄σj = ν̄σk4 .
Notice that this blocking condition is looser than the blocking condition introduced in
Definition 5 for a SHOIQ-forest. Since we cannot determine the path from root to a
node satisfying a star-type over a frame, it is 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 E XP S PACE tableau-based algorithm for SHOIQ.
It starts by generating nominal star-types at level 0. The goal of the algorithm is to
replace progressively non-valid star-types with those which are “nearer” the validity.
When a non-valid star-type σ at a level h is replaced with a “better” one σ 0 at the same
level, the algorithm adds δ(σ) to δ(σ 0 ) and sets δ(σ) = 0. This may lead to update δ(ω)
where ω is linkable with σ. In addition, the algorithm has to maintain two functions
Φ(σ) and δ(Φ(σ))
b such that the conditions 5 and 6 in Definition 9 always hold after
each update of star-types.
An important difference between the tableau algorithm presented in Section 3 and
the tableau algorithm for constructing a valid frame is that the latter adds star-types to a
frame and updates functions δ(σ) and δ(Φ(σ))
b instead of adding nodes for representing
individuals. Again, we refer the readers to [5] where the rules for building a valid frame,
called frame rules, can be found.
Soundness of the tableau-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 tableau algorithm for con-
structing a frame is a decision procedure for consistency of (T , R) and it runs in E X -
P S PACE in the size of (T , R).
5 Conclusion and Discussion
We have presented in this paper a practical E XP S PACE 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 trans-
ferred to SHOIQ the method used for constructing a NE XP T IME algorithm for C 2 .
This enables us to represent a doubly exponential SHOIQ-forest by an exponential
structure.
The tableau algorithms proposed in the present paper have introduced several new
non-deterministic rules, e.g., ./- or ≤o -rules. In particular, the most non-deterministic
behaviour of the tableau algorithm for building a valid frame is to update the function
δ for star-types ω when applying frame rules to a star-type σ which is linkable with ω.
Such an update may lead to choose a subset from an exponential set of linkable star-
types. An open issue consists in investigating whether the complexity resulting from
this behaviour is comparable to that caused by the ≤- and ≤o -rules.
Acknowledgements. Thanks to the reviewers for their helpful comments.
References
1. Horrocks, I.: The FaCT system. In: de Swart, H. (ed.) Proc. of the 2nd Int. Conf. on Analytic
Tableaux and Related Methods (TABLEAUX’98). Lecture Notes in Artificial Intelligence,
vol. 1397, pp. 307–312. Springer (1998), download/1998/Horr98b.pdf
2. Horrocks, I., Sattler, U.: A tableau decision procedure for SHOIQ. Journal Of Automated
Reasoning 39(3), 249–276 (2007)
3. Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for expressive description logics. In:
Proceedings of the International Conference on Logic for Programming, Artificial Intelligence
and Reasoning (LPAR 1999). Springer (1999)
4. Kazakov, Y., Motik, B.: A resolution-based decision procedure for SHOIQ. Journal of Au-
tomated Reasoning 40(2–3), 89–116 (2008)
5. Le Duc, C., Lamolle, M., Curé, O.: An EXPSPACE tableau-based algorithm for SHOIQ. In:
Technical Report. http://www.iut.univ-paris8.fr/∼leduc/papers/RR2012a.pdf (2012)
6. Patel-Schneider, P., Hayes, P., Horrocks, I.: OWL web ontology language semantics and ab-
stract syntax. In: W3C Recommendation (2004)
7. Pratt-Hartmann, I.: Complexity of the two-variable fragment with counting quantifiers. Jour-
nal of Logic, Language and Information 14(3), 369–395 (2005)
8. Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: a pratical OWL-DL reasoner.
Journal of Web Semantics 5(2), 51–53 (2007)
9. Tobies, S.: The complexity of reasoning with cardinality restrictions and nominals in expres-
sive description logics. Journal of Artificial Intelligence Research 12, 199–217 (2000)