=Paper=
{{Paper
|id=None
|storemode=property
|title=SHOIQ with Transitive Closure of Roles Is Decidable
|pdfUrl=https://ceur-ws.org/Vol-1014/paper_89.pdf
|volume=Vol-1014
|dblpUrl=https://dblp.org/rec/conf/dlog/DucLC13
}}
==SHOIQ with Transitive Closure of Roles Is Decidable==
https://ceur-ws.org/Vol-1014/paper_89.pdf
SHOIQ with transitive closure of roles is decidable
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. The Semantic Web makes an extensive use of the OWL DL ontology
language, underlied by the SHOIQ description logic, to formalize its resources.
In this paper, we propose a decision procedure for this logic extended with the
transitive closure of roles in concept axioms, a feature needed in several applica-
tion domains. To address the problem of consistency in this logic, we introduce a
new structure for characterizing models which may have an infinite non-tree-like
part.
1 Introduction
The ontology language OWL-DL [1] is widely used to formalize data resources on the
Semantic Web. This language is mainly based on the description logic SHOIN which
is known to be decidable [2]. Although SHOIN provides transitive roles to model
transitivity of relations, we can find several applications in which the transitive closure
of roles, that is more expressive than transitive roles, is needed. For instance, if we
denote by R− and R+ the inverse and transitive closure of a role R respectively then
it is obvious that the concept ∃R+ .∀R− .⊥ is unsatisfiable w.r.t. an empty TBox. If we
now substitute R+ for a transitive role Rt such that R v Rt (i.e. we substitute each
occurrence of R+ in axioms for Rt ) then the concept ∃Rt .∀R− .⊥ is satisfiable. The
point is that an instance of R+ represents a sequence of instances of R but an instance
of Rt corresponds to a sequence of instances of itself.
In this paper, we consider an extension of SHOIQ by enabling transitive closure
of roles in concept axioms. In the general case, transitive closure is not expressible in
the first order logic [3], the logic from which DL is a sublanguage, while the second
order logic is sufficiently expressive to do so.
In the DL literature ([4]; [5]), there have been works dealing with transitive closure
of roles. Recently, Ortiz [5] has proposed an algorithm for deciding consistency in the
logic ALCQIb+ reg which allows for transitive closure of roles. However, nominals are
disallowed in this logic. It is known that reasoning with a DL including number restric-
tions, inverse roles, nominals and transitive closure of roles is hard. The reason for this
is that there exists an ontology in that DL whose models have an infinite non-tree-like
part. Calvanese et al. [6] have presented an automata-based technique for dealing with
the logic ZOIQ that includes transitive closure of roles, and showed that the sublogics
ZIQ, ZOQ and ZOI are decidable. To obtain this result, the authors have introduced
the quasi-forest model property to characterize models of ontologies in these sublogics.
Although they are very expressive, none of these sublogics includes SHOIQ with tran-
sitive closure of roles, namely SHOIQ(+) . The following example3 , noted K1 , shows
that there is an ontology in SHOIQ(+) which does not enjoy the quasi-forest model
property. We consider the following axioms:
(1) {o} v A; A u B v ⊥; A v ∃R.A u ∃R0 .B; B v ∃S+ .{o}
(2) {o} v ∀X− .⊥; > v ≤ 1 X.>; > v ≤ 1 X− .> where X ∈ {R, R0 , S}
Figure 1 shows an infinite non-tree-like model of K1 . In fact, each individual x that sat-
isfies ∃S+ .{o} must have two distinct paths from x to the individual satisfying nominal
o. Intuitively, we can see that (i) such a x must satisfy ∃S+ .{o} and B, (ii) an individual
satisfying B must connect to another individual satisfying A which must have a R-path
to nominal o, and (iii) two concepts A and B are disjoint.
{o}, A R A R A R A
R0 , S − R0 R0
S− S− S−
B, ∃S + .{o} B, ∃S + .{o} B, ∃S + .{o} B, ∃S + .{o}
Fig. 1. An infinite non tree-like model of K1
This example shows that methods ([7], [8], [6]) based on the hypothesis which says
that if an ontology is consistent it has a quasi-forest model, could fail to address the
problem of consistency in a DL including simultaneously O (nominals), I (inverse
roles), Q (number restrictions) and transitive closure of roles.
In this paper, we propose a decision procedure for the problem of consistency in
SHOIQ with transitive closure of roles in concept axioms. The underlying idea of our
algorithm is founded on the star-type and frame notions introduced by Pratt-Hartmann
[9]. This technique uses star-types to represent individuals and “tiles” them together
to form a frame for representing a model. For each star-type σ, we maintain a func-
tion δ(σ) which stores the number of individuals satisfying this star-type. To obtain
termination condition, we introduce two additional structures into a frame : (i) the first
one, namely cycles, describes duplicate parts of a model resulting from interactions of
logic constructors in SHOIQ, (ii) the second one, namely blocking-blocked cycles,
describes parts of a model bordered by cycles which allow a frame to satisfy transitive
closure of roles occurring in concepts of the form ∃R+ .C.
2 The Description Logic SHOIQ(+)
In this section, we present the syntax, the semantics and main inference problems of
SHOIQ(+) . In addition, we introduce a tableau structure for SHOIQ(+) , which al-
lows us to represent a model of a SHOIQ(+) knowledge base.
3
This example is initially proposed by Sebastian Rudolph from an informal discussion
Definition 1. Let R be a non-empty set of role names and R+ ⊆ R be a set of tran-
sitive role names. We use RI = {P − | P ∈ R} to denote a set of inverse roles, and
R⊕ = {Q+ | Q ∈ R ∪ RI } to denote a set of transitive closure of roles. Each element
of R ∪ RI ∪ R⊕ is called a SHOIQ(+) -role. A role inclusion axiom is of the form
R v S for two SHOIQ(+) -roles R and S such that R ∈ / R⊕ and S ∈ / R⊕ . A role
hierarchy R is a finite set of role inclusion axioms. 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
I
R− = {hx, yi ∈ ∆I × ∆I | hy, xi ∈ RI } for all R ∈ R,
hx, zi ∈ S I , hz, yi ∈ S I [
implies hx, yi ∈ S I for each S ∈ R+ , and
+ I
(Q ) = (Qn )I with (Q1 )I = QI ,
n>0
(Qn )I = {hx, yi ∈ (∆I )2 | ∃z ∈ ∆I , hx, zi ∈ (Qn−1 )I , hz, yi ∈ QI } for Q+ ∈ R⊕
∗ An 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. To simplify notations
for nested inverse roles and transitive closures of roles, we define two functions · and
·⊕ as follows:
− +
R
if R ∈ R; R+
if R ∈ R;
S if R = S − and S ∈ R; ⊕ S if R = (S + )+ and S ∈ R;
R = − + + R = − + −
(S+ ) if R = S −, S+ ∈ R,
(S − )+ if R = S +and
S ∈ R;
S if R = (S ) , S ∈ R (S ) if R = (S )− and S ∈ R
∗ A relation v∗ is defined as the transitive-reflexive closure R+ of v on R ∪ {R v
S | R v S ∈ R} ∪ {R⊕ v S ⊕ | R v S ∈ R} ∪ {Q v Q⊕ | Q ∈ R ∪ RI }. We
define a function Trans(R) which returns true iff there is some Q ∈ R+ ∪ {P | P ∈
R+ } ∪ {P ⊕ | P ∈ R ∪ RI } such that QvR ∗ ∈ R+ . A role R is called simple w.r.t. R
if Trans(R) = false.
The reason for the introduction of two functions · and ·⊕ in Definition 1 is that
they avoid using R−− and R++ . Moreover, it remains a unique nested case (R− )+ .
According to Definition 1, axiom R v Q⊕ is not allowed in a role hierarchy R since
this may lead to undecidability [10]. Notice that the closure R+ may contain R v Q⊕
if R v Q belongs to 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, >, C u D, C t 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 u D)I = C I ∩ DI ,
(C tD)I = C I ∪DI , (¬C)I = ∆I \C I , |{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 | |{y ∈ C I | hx, yi ∈ S I | ≥ n},
(≤ n S.C)I = {x ∈ ∆I | |{y ∈ C I | hx, yi ∈ S I | ≤ n} where |S| is denoted for the
cardinality of a set S. An axiom 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 . 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 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). C
Since unsatisfiability, subsumption and consistency w.r.t. a SHOIQ(+) knowledge
base can be reduced to each other, 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 equiva-
lences as presented in [11]. According to [12], 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 a 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
reuse cl(T , R), which was introduced by Horrocks et al. [7], to denote all sub-concepts
occurring in the axioms of (T , R). We have cl(T , R) is bounded by O(|(T , R)|) [7].
To translate star-type and frame structures presented by Pratt-Hartmann (2005) for C 2
into those for SHOIQ, we need to add new sets of concepts, denoted cl1 (T , R) and
cl2 (T , R), to the signature of a SHOIQ(+) knowledge base (T , R).
cl1 (T , R) = {≤ mS.C | {(≤ nS.C), (≥ nS.C)} ∩ cl(T , R) 6= ∅, 1 ≤ m ≤ n} ∪
{≥ mS.C | {(≤ nS.C), (≥ nS.C)} ∩ cl(T , R) 6= ∅, 1 ≤ m ≤ n}
For a generating
l concept (≥
l nS.C) and a set I ⊆ {0, · · · , log n + 1}, we denote
j
C(≥nS.C)
I
= i
C(≥nS.C) u ¬C(≥nS.C) i
where C(≥nS.C) are new concept names
i∈I j ∈I
/
for 0 ≤ i ≤ log n + 1. We define cl2 (T , R) as follows:
i
cl2 (T , R) = {C(≥S.C) | (≥ nS.C) ∈ cl(T , R) ∪ cl1 (T , R), 0 ≤ i ≤ log n + 1}∪
I
{C(≥nS.C) | (≥ nS.C) ∈ cl(T , R) ∪ cl1 (T , R), I ⊆ {0,· · ·, log n + 1}}
Remark 1. If numbers are encoded in binary then the number of new concept names
i
C(≥nS.D) for 0 ≤ i ≤ log n + 1, is bounded by O(|(T , R)|) since n is bounded by
|(T ,R)|
O(2 ). This implies that |cl2 (T , R)| is bounded by O(2|(T ,R)| ). Note that two
concepts C(≥nS.C)
I
and C(≥nS.C)
J
are disjoint for all I, J ⊆ {0, · · · , log n + 1}, I 6= J.
The concepts C(∃S.C) and C(≥nS.C)
I
will be used for building chromatic star-types. This
notion will be clarified after introducing the frame structure (Definition 5).
Finally, we denote CL(T , R) = cl(T , R) ∪ cl1 (T , R) ∪ cl2 (T , R), and 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 [13].
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, if
∀S.C is a sub-concept from T and RvS ∗ ∈ R then ∀R.C ∈ CL(T , R).
To describe a model of a SHOIQ(+) knowledge base in a more intuitive way, we
use a tableau structure that expresses semantic constraints resulting directly from the
logic constructors in SHOIQ(+) . A tableau definition for SHOIQ(+) can be found
in [14].
3 A Decision Procedure For SHOIQ(+)
This section starts by translating star-type and frame structures presented by Pratt-
Hartmann (2005) for C 2 into those for SHOIQ(+) .
Definition 3 (star-type). Let (T , R) be a SHOIQ(+) knowledge base. A star-type
is a pair σ = hλ(σ), ξ(σ)i, where λ(σ) ∈ 2CL(T ,R) is called core label, ξ(σ) =
(hr1 , l1 i, · · · , hrd , ld i) is a d-tuple over 2R(T ,R) × 2CL(T ,R) . A pair hr, li is a ray of
σ if hr, li = hri , li i for some 1 ≤ i ≤ d. We use hr(ρ), l(ρ)i to denote a ray ρ = hr, li
where r(ρ) = r and l(ρ) = l.
– A star-type σ is nominal if o ∈ λ(σ) for some o ∈ Co .
– A star-type σ is chromatic if ρ 6= ρ0 implies l(ρ) 6= l(ρ0 ) for two rays ρ, ρ0 of σ.
When a star-type σ is chromatic, ξ(σ) can be considered as a set of rays.
– Two star-types σ, σ 0 are equivalent if λ(σ) = λ(σ 0 ), and there is a bijection π
between ξ(σ) and ξ(σ 0 ) such that π(ρ) = ρ0 implies r(ρ0 ) = r(ρ) and l(ρ0 ) = l(ρ).
We denote Σ for the set of all star-types for (T , R). C
Note that for a chromatic star-type σ, ξ(σ) can be considered as a set of rays since
rays are distinct and not ordered. We can think of a star-type σ as the set of individuals
x satisfying all concepts in λ(σ), and each ray ρ of σ corresponds to a “neighbor”
individual xi of x such that r(ρ) is the label of the link between x and xi ; and xi
satisfies all concepts in l(ρ). In this case, we say that x satisfies σ.
Definition 4 (valid star-type). Let (T , R) be a SHOIQ(+) knowledge base. Let σ be
a star-type for (T , R) where σ = hλ(σ), ξ(σ)i. The star-type σ is valid if σ is chromatic
and the following conditions are satisfied:
1. If C v D ∈ T then nnf(¬C t D) ∈ λ(σ);
2. {A, ¬A} 6⊆ λ for every concept name A where λ = λ(σ) or λ = l(ρ) for each
ρ ∈ ξ(σ);
3. If C1 u C2 ∈ λ(σ) then {C1 , C2 } ⊆ λ(σ);
4. If C1 t C2 ∈ λ(σ) then {C1 , C2 } ∩ λ(σ) 6= ∅;
5. If ∃R.C ∈ λ(σ) then there is some ray ρ ∈ ξ(σ) such that C ∈ l(ρ) and R ∈ r(ρ);
6. If (≤ nS.C) ∈ λ(σ) and there is some ray ρ ∈ ξ(σ) such that S ∈ r(ρ) then
C ∈ l(ρ) or ¬C
˙ ∈ l(ρ);
7. If (≤ nS.C) ∈ λ(σ) and there is some ray ρ ∈ ξ(σ) such that C ∈ l(ρ) and S ∈
r(ρ) then there is some 1 ≤ m ≤ n such that {(≤ mS.C), (≥ mS.C)} ⊆ λ(σ);
8. For each ray ρ ∈ ξ(σ), if R ∈ r(ρ) and RvS∗ then S ∈ r(ρ);
9. If ∀R.C ∈ λ(σ) and R ∈ r(ρ) for some ray ρ ∈ ξ(σ) then C ∈ l(ρ);
10. If ∀R.D ∈ λ(σ), S vR, ∗ Trans(S) and R ∈ r(ρ) for some ray ρ ∈ ξ(σ) then
∀S.D ∈ l(ρ);
11. If ∀Q⊕ .C ∈ λ(σ), RvQ ∗ and R ∈ r(ρ) for some ray ρ ∈ ξ(σ) then ∀Q⊕ .C ∈ l(ρ);
12. If ∃Q .C ∈ λ(σ) then (∃Q.C t ∃Q.∃Q⊕ .C) ∈ λ(σ);
⊕
13. If (≥ nS.C) ∈ λ(σ) then there are n distinct rays ρ1 , · · · , ρn ∈ ξ(σ) such that
{C, C(≥nS.C)
Ii
} ⊆ l(ρi ), S ∈ r(ρi ) for all 1 ≤ i ≤ n; and Ij , Ik ⊆ {0, · · · , log n +
1}, Ij 6= Ik for all 1 ≤ j < k ≤ n.
14. If (≤ nS.C) ∈ λ(σ) and there do not exist n + 1 rays ρ0 , · · · , ρn ∈ ξ(σ) such that
C ∈ l(ρi ) and S ∈ r(ρi ) for all 0 ≤ i ≤ n. C
Roughly speaking, a star-type σ is valid if each individual x satisfies semantically
all concepts in λ(σ). In fact, each condition in Definition 4 represents the semantics of a
constructor in SHOIQ(+) except for transitive closure of roles. From valid star-types,
we can “tile” a model instead of using expansion rules for generating nodes as described
in tableau algorithms. Before presenting how to “tile” a model from star-types, we need
some notation that will be used in the remainder of the paper.
Notation 1 We call P = h(σ1 , ρ1 , d1 ), · · · , (σk , ρk , dk )i a sequence where σi ∈ Σ,
ρi ∈ ξ(σi ) and di ∈ N for 1 ≤ i ≤ k.
– tail(P) = (σk , ρk , dk ), tailσ (P) = σk , tailρ (P) = ρk , tailδ (P) = dk and |P| = k.
We denote L(P) = λ(tailσ (P)).
– pi (P) = (σi , ρi , di ), piσ (P) = σi , piρ (P) = ρi and piδ (P) = di for each 1 ≤ i ≤ k.
– an operation add(P, (σ, ρ, d)) extends P to a new sequence with add(P, (σ, ρ, d)) =
hP, (σ, ρ, d)i.
Definition 5 (frame). Let (T , R) be a SHOIQ(+) knowledge base. A frame for (T , R)
is a tuple F = hN , No , Ω, δi, where
1. N is a set of valid star-types such that σ is not equivalent to σ 0 for all σ, σ 0 ∈ N ;
2. No ⊆ N is a set of nominal star-types;
3. Ω is a function that maps each pair (σ, ρ) with σ ∈ N and ρ ∈ ξ(σ) to a sequence
Ω(σ, ρ) = h(σ1 , ρ1 , d1 ), · · · , (σm , ρm , dm )i with σi ∈ N , ρi ∈ ξ(σi ), di ∈ N for
1 ≤ i ≤ m such that for each σi with 1 ≤ i ≤ m, it holds that l(ρ) = λ(σi ),
l(ρi ) = λ(σ) and r(ρi ) = r− (ρ) where r− (ρ) = {R | R ∈ r(ρ)}.
4. δ is a function δ : N → N. By abuse of notation, we also use δ to denote a function
which maps each pair (σ, ρ) with σ ∈ N and ρ ∈ ξ(σ) into a number in N, i.e.,
δ(σ, ρ) ∈ N. C
The frame structure, as introduced in Definition 5, allows us to compress individuals
of a model into star-types. For each star-type σ and each ray ρ ∈ ξ(σ), a list Ω(σ, ρ) of
triples (σi , ρi , di ) with ρi ∈ ξ(σi ) is maintained where σi is a “neighbor” star-type of
σ via ρ ∈ ξ(σ), and di indicates the di -th “layer” of rays of σi . We can think a layer of
rays of σi as an individual that connects to its neighbor individuals via the rays of σi .
The following definition presents how to connect such layers to form paths in a frame.
Definition 6 (path). Let F = hN , No , Ω, δi be a frame for a SHOIQ(+) knowledge
base (T , R). A path is inductively defined as follows:
1. A sequence h∅, (σ, ρ, 1)i is a path if σ ∈ No and ρ ∈ ξ(σ);
2. A sequence hP, (σ, ρ, d)i with P = 6 ∅ and tail(P) = (σ0 , ρ0 , d0 ), is a path if
(σ, ρ, d) = pd0 (Ω(σ0 , ρ0 )) for each ρ0 6= ρ0 . In this case, we say that hP, (σ, ρ, d)i
is the ρ0 -neighbor of P, and two paths P, hP, (σ, ρ, d)i are neighbors.
Additionally, if hP, (σ, ρ, d)i is a ρ0 -neighbor of P and Q ∈ r(ρ0 ) then hP, (σ, ρ, d)i
is a Q-neighbor of P. In this case, we say that hP, (σ, ρ, d)i is a Q-neighbor of P,
or P is a Q -neighbor of hP, (σ, ρ, d)i.
We define P ∼ P 0 if tailσ (P) = tailσ (P 0 ) and tailδ (P) = tailδ (P 0 ). Since ∼ is an
equivalence relation over the set of all paths, we use P to denote the set of all equiva-
lence classes [P] of paths in F. For [P], [Q] ∈ P, we define:
1. [P] is a neighbor (ρ0 -neighbor) of [Q] if there are P 0 ∈ [P] and Q0 ∈ [Q] such that
Q0 is a neighbor (ρ0 -neighbor) of P 0 ;
2. [Q] is a reachable path of [P] if there are [P1 ], · · · , [Pn ] ∈ P such that [Pi+1 ] is
a neighbor of [Pi ] for all 1 ≤ i < n where [P1 ] = [P] and [Q] = [Pn ].
3. [Q] is a Q-neighbor of [P] if there are P 0 ∈ [P] and Q0 ∈ [Q] such that Q0 is a
Q-neighbor of P 0 , or P 0 is a Q -neighbor of Q0 ;
4. [Q] is a Q-reachable path of [P] if there are [P1 ], · · · , [Pn ] ∈ P such that [Pi+1 ]
is a Q-neighbor of [Pi ] for all 1 ≤ i < n where [P1 ] = [P] and [Q] = [Pn ]. C
Note that for two paths P, P 0 with tailρ (P) 6= tailρ (P 0 ), we have P ∼ P 0 if
tailσ (P) = tailσ (P 0 ) and tailδ (P) = tailδ (P 0 ). This does not allow for extending
tailρ (P) to tailρ ([P]). As a consequence, there may be several “predecessors” of an
equivalence class [P]. However, we can define tailσ ([P]) = tailσ (P), tailδ ([P]) =
tailδ (P) and L([P]) = L(P). In the sequel, we use P instead of [P] whenever it is
clear from the context.
Definition 7 (cycle). Let F = hN , No , Ω, δi be a frame for a SHOIQ(+) knowledge
base (T , R) with a set P of paths in F.
1. A cycle is a set Θ of triples (P, ρ, Q) with P, Q ∈ P and ρ ∈ ξ(tailσ (P)) such
that for each (P, ρ, Q) ∈ Θ the following conditions are satisfied:
(a) tailδ (P) > 1 and tailδ (Q) > 1;
(b) If P 0 is the ρ-neighbor of P then tailσ (P 0 ) = tailσ (Q);
(c) for each sequence P1 , · · · , Pn ∈ P such that P1 = P, P2 is not the ρ-
neighbor of P, and Pi+1 is a neighbor of Pi for 1 ≤ i < n, there is some
(P 00 , ρ00 , Q00 ) ∈ Θ such that
i. either Q00 = Pj , tailσ (Pj+1 ) = tailσ (P 00 ), tailδ (Pj+1 ) ≥ tailδ (P 00 ) and
Pj is the ρ-neighbor of Pj+1 for some 1 < j < n,
ii. or there are Pn+1 , · · · , Pn+m ∈ P with Q00 = Pn+m−1 , tailσ (Pn+m ) =
tailσ (P 00 ), tailδ (Pn+m ) ≥ tailδ (P 00 ) and Pi+1 is a neighbor of Pi for
n ≤ i < n + m.
In this case, we say that Q is cycled by P via ρ.
2. A cycle Θ0 is a reachable cycle of Θ if for each (P, ρ, Q) ∈ Θ and for each sequence
P1 , · · · , Pn ∈ P such that P1 = P, P2 is not a ρ-neighbor of P, and Pi+1 is a
neighbor of Pi for 1 ≤ i < n, there is some (P 00 , ρ00 , Q00 ) ∈ Θ0 such that
(a) either Q00 = Pj , tailσ (Pj+1 ) = tailσ (P 00 ), tailδ (Pj+1 ) ≥ tailδ (P 00 ) and Pj is
a ρ-neighbor of Pj+1 for some 1 < j < n,
(b) or there are Pn+1 , · · · , Pn+m ∈ P with Q00 = Pn+m−1 , tailσ (Pn+m ) =
tailσ (P 00 ), tailδ (Pn+m ) ≥ tailδ (P 00 ) and Pi+1 is a neighbor of Pi for n ≤ i <
n + m. C
Note that cycles may encapsulate loops if tailδ (Pj+1 ) = tailδ (P 00 ) holds in Condi-
tions 1(c)i and 1(c)ii, Definition 7. Let Θ be a cycle in a frame. Definition 7 ensures
that each reachable path of some path P with (P, ρ, Q) ∈ Θ goes through a star-type
σ = tailσ (Q0 ) with some (P 0 , ρ0 , Q0 ) ∈ Θ. Such a cycle, which is similar to blocking-
blocked nodes in completion graphs for SHOIQ [7], allows for “unravelling” infinitely
the frame to obtain a model of a KB in SHOIQ (without transitive closure of roles).
This means that we can extend the set P of paths by adding infinitely paths which
lengthen Q such that (P, ρ, Q) ∈ Θ and P is not a neighbor of Q. However, such a cy-
cle structure is not sufficient to represent models of a KB with transitive closure of roles
since a concept such as ∃Q⊕ .D ∈ L(P) can be satisfied by a Q-reachable path P 0 of
P which is arbitrarily far from P. There are the following possibilities for an algorithm
which builds a frame: (i) the algorithm stops building the frame as soon as a cycle Θ
is detected such that each concept of the form ∃Q⊕ .D occurring in L(P) for each cy-
cling path P of Θ is satisfied, i.e., P has a Q-reachable path P 0 with ∈ ∃Q.D ∈ L(P),
(ii) despite of several detected cycles, the algorithm continues building the frame un-
til each concept of the form ∃Q⊕ .D occurring in L(P) is satisfied for each cycling
path P of Θ. If we adopt the first possibility, the completeness of such an algorithm
cannot be established since there are models in which paths satisfying concepts of the
form ∃Q⊕ .D can spread over several “iterative structures” such as cycles. For this rea-
son, we adopt the second possibility by introducing into frames an additional structure,
namely blocking-blocked cycles, which determines a sequence of cycles Θ1 , · · · , Θk
such that Θi+1 is a reachable cycle of Θi . Reachability of cycles allows for “unravel-
ling” the frame between cycled paths Q0 with (P 0 , ρ0 , Q0 ) ∈ Θk and cycling paths P
with (P, ρ, Q) ∈ Θ1 .
Definition 8 (blocking). Let F = hN , No , Ω, δi be a frame for a SHOIQ(+) knowl-
edge base (T , R) with a set P of all paths in F.
1. A cycle Θ0 is blockable by a cycle Θ if Θ0 is a reachable cycle of Θ, and for
each (P 0 , ρ0 , Q0 ) ∈ Θ0 there is some (P, ρ, Q) ∈ Θ such that L(P) = L(P 0 ),
L(Q) = L(Q0 ) and r(ρ) = r(ρ0 ). In this case, we say that Q0 is blockable by P
via ρ.
2. A cycle Θ0 is blocked by a cycle Θ if there are Θ1 , · · · , Θk with Θ = Θ1 , Θ0 =
Θk such that Θi+1 is blockable by Θi for 1 ≤ i < k, and for each (λ, s, λ0 ) ∈
2CL(T ,R) × 2R(T ,R) × 2CL(T ,R) with ∃Q⊕ .D ∈ λ,
– if there is some path Pk with (Pk , ρk , Qk ) ∈ Θk , L(Pk ) = λ, L(Qk ) = λ0 ,
s = r(ρk ) such that Pk has no Q-reachable path Pk0 with ∃Q.D ∈ L(Pk0 ),
– then there is some P1 with (P1 , ρ1 , Q1 ) ∈ Θ1 , L(P1 ) = λ, L(Q1 ) = λ0 ,
r(ρ1 ) = s such that for each ∃P ⊕ .C ∈ L(P1 ),
• there is a P -reachable path Q00 of P1 with ∃P.C ∈ L(Q00 ), and
• there are two triples (Pj , ρj , Qj ) ∈ Θj and (Pj+1 , ρj+1 , Qj+1 ) ∈ Θj+1
for some 1 ≤ j < k,
which satisfy that Q00 is a reachable path of Qj and Qj+1 is a reachable path
of Q00 .
In this case, we say that P1 blocks Pk via ρk . C
According to Definition 8, there are a sequentially reachable cycles between a
blocking cycle Θ1 and a blocked cycle Θk , which allows for unravelling the frame
between Θk and Θ1 . Condition 2 Definition 8 says that if (P, ρ, Q) ∈ Θk and L(P)
contains concepts of the form ∃Q⊕ .D which are not satisfied by reachable paths of P
then there exists some P 0 with (P 0 , ρ0 , Q0 ) ∈ Θ1 which allows for satisfying these con-
cepts ∃Q⊕ .D in L(P) by unravelling. We would like to note that a path P is blocked if
there is some blocked cycle Θk such that (P, ρ, Q) ∈ Θk .
Definition 9 (valid frame). Let (T , R) be a SHOIQ knowledge base. A frame F =
hN , No , Ω, δi is valid if the following conditions are satisfied:
1. For each o ∈ Co there is a unique σo ∈ No such that o ∈ λ(σo ) and δ(σo ) = 1;
2. For each σ ∈ N , σ is valid;
3. If ∃Q⊕ .C ∈ λ(tailσ (P0 )) for some P0 ∈ P then there are P, P 0 ∈ P such that
one of the following conditions is satisfied:
(a) P0 = P = P 0 and ∃Q.C ∈ L(P0 );
(b) P 0 is a Q-reachable of P, and ∃Q.C ∈ L(P 0 ) where P = P0 or P blocks P0 ;
(c) P is a Q -reachable of P 0 , and ∃Q.C ∈ L(P 0 ) where P = P0 or P blocks
P0 . C
Conditions 1-3 in Definition 9 ensure satisfaction of tableau properties [14]. In par-
ticular, Condition 3 takes into account satisfaction of transitive closure of roles. In fact,
for each blocking path P with ∃Q⊕ .D ∈ L(P), this condition says that P must be
satisfied by a Q-reachable path P 0 of P between a blocking cycle Θ1 and a blocked
cycle Θk . If there is some path Q between Θ1 and Θk with ∃S ⊕ .C ∈ L(Q) that is not
satisfied, due to the construction of star-types and frames, a concept ∃S ⊕ .C is prop-
agated along S-reachable paths of Q. This implies that Q has a S-reachable path Q0
such that Q0 is blocked and ∃S ⊕ .C ∈ L(Q0 ). By unravelling (details will be given
in soundness proof), we can build an (extended) S-reachable path Q00 of Q0 such that
∃S.C ∈ L(Q00 ).
We now present Algorithm 1 for building a frame which is valid if the conditions
in Definition 9 are satisfied. This algorithm starts by adding nominal star-types to the
frame. For each non blocked path P with a ray ρ ∈ ξ(tailσ (P)) such that δ(tailσ (P)) is
minimal and there is a difference between δ(tailσ (P)) and δ(tailσ (P), ρ), the algorithm
picks in a nondeterministic way a valid star-type ω that matches tailσ (P) via ρ, and
updates Ω(tailσ (P), ρ), Ω(ω, ρ0 ), δ(tailσ (P), ρ), δ(ω, ρ0 ), eventually, δ(tailσ (P)) and
δ(ω) by calling updateFrame(· · · )[14]. The algorithm terminates when a blocked cycle
is detected.
Figure 2 depicts a frame when executing Algorithm 1 for K1 in the example pre-
sented in Section 1. The algorithm builds a frame F = hN , No , Ω, δi where N =
{σ0 , σ1 , σ2 , σ3 , σ4 } and No = {σ0 }. The dashed arrows indicate how the function
Require: A SHOIQ(+) knowledge base (T , R)
Ensure: A frame hN , No , Ω, δi for (T , R)
1: Let Σ be the set of all star-types for (T , R)
2: for all o ∈ Co do
3: if there is no σ ∈ N such that o ∈ λ(σ) then
4: Choose a star-type σo ∈ Σ such that o ∈ λ(σo )
5: Set δ(σo ) = 1, N = N ∪ {σo } and No = No ∪ {σo }
6: Set δ(σo , ρ) = 0, Ω(σo , ρ) = ∅ for all ρ ∈ ξ(σo )
7: end if
8: end for
9: while there is a path P that is not blocked and a ray ρ ∈ ξ(tailσ (P)) such that
tailδ (P) = δ(tailσ (P), ρ) + 1 and δ(tailσ (P)) ≤ δ(ω) for all ω ∈ N do
10: Choose a star-type σ 0 ∈ Σ such that there is a ray ρ0 ∈ ξ(σ 0 ) satisfying
l(ρ) = λ(σ 0 ), l(ρ0 ) = λ(σ), r(ρ0 ) = r− (ρ), and
σ 0 ∈ N implies δ(σ 0 ) = δ(σ 0 , ρ0 ) + 1
11: updateFrame(σ, ρ, σ 0 , ρ0 )
12: end while
Algorithm 1: An algorithm for building a frame
Ω(σ, ρ) can be built. For example, Ω(σ0 , ρ0 ) = {(σ1 , ν0 , 1)}, Ω(σ0 , ρ1 ) = {(σ2 , ρ00 , 1)}
where ρ0 and ρ1 are the respective horizontal and vertical rays of σ0 ; ν0 is the left ray of
σ1 ; ρ00 is the vertical ray of σ2 . Moreover, the directed dashed arrow from σ0 to σ1 indi-
cates that the ray ρ0 of σ0 can match the ray ν0 on the left ray of σ1 since l(ρ0 ) = λ(σ1 ),
r(ν0 ) = λ(σ0 ), r(ν0 ) = r− (ρ0 ).
Then, the algorithm generates δ(σ0 ) = 1, δ(σ1 ) = 1, δ(σ2 ) = 1 and forms a cycle
Θ consisting of the following triples : ((σ3 , 2), ρ1 , (σ3 , 3)) (ρ1 is the left ray of σ3 )),
((σ3 , 2), ρ3 , (σ4 , 1)) (ρ3 is the vertical ray of σ3 ), ((σ4 , 1), ρ4 , (σ4 , 2)) (ρ4 is the left ray
of σ4 ) and ((σ4 , 1), ρ5 , (σ3 , 2)) (ρ5 is the vertical ray of σ4 ). Note that for the sake of
brevity, we use just tailσ (P) and tailδ (P) to denote a path in the triples. We can check
that any path that is an extension of a path P gets through a path Q where P is the first
component of a triple and Q is the third component of a triple.
The algorithm may add some more paths that go through σ3 and σ4 to form a
blocked cycle. A model of the ontology can be built by starting from σ0 and getting
(i) σ4 via σ1 , (ii) σ3 via σ1 , and (iii) σ3 via σ2 . From σ3 and σ4 , the model goes through
σ3 and σ4 infinitely. Note that from any individual x satisfying σ3 (or σ4 ), i.e. the “la-
bel” of x contains ∃Q+ .{o}, there is a path containing S which goes back the individual
satisfying σ0 . Thus, the concept ∃Q+ .{o} is satisfied for each individual whose label
contains ∃Q+ .{o}.
Lemma 1. Let (T , R) be a SHOIQ(+) knowledge base.
1. Algorithm 1 terminates.
2. If Algorithm 1 can build a valid frame for (T , R) then (T , R) is consistent.
3. If (T , R) is consistent then Algorithm 1 can build a valid frame F for (T , R).
Proof (sketch). Since the functions δ(σ) and δ(σ, hr, li) is increased monotonously by
Algorithm 1, termination of the algorithm can be proved if we can show that : (i) the
{o}, A R− A R A
σ1
{o}, A R A
R0 A R− A R A
σ0 A σ4
R , S−
0 {o}, A
B, ∃S + .{o} R0
R0−
R0− , S σ3 B, ∃S + .{o}
B, ∃S + .{o} S S−
σ2
S− B, ∃S + .{o} +
B, ∃S .{o} B, ∃S + .{o}
+
B, ∃S .{o} B, ∃S + .{o}
Fig. 2. A frame obtained by Algorithm 1 for K1 in the example in Section 1
number of different star-types is bounded; (ii) the detection of a blocked cycle accord-
ing to Definition 8 terminates. For the soundness of Algorithm 1, we can extend the set
P of paths to a set P c of extended paths by “unravelling” the frame between blocking-
blocked cycles. A tableau [14] can be built from P. c The main argument is that when
extending a path P if tailσ (P) 6= tailσ (P ) for all blocked path P 0 then this exten-
0
sion process can be continued up to a star-type σ 0 = tailσ (P 00 ) for some blocked path
P 00 . This holds due to the definition of cycles and blockable cycles. Otherwise, i.e.,
tailσ (P) = tailσ (P 0 ) for some blocked path P 0 by Q then P can be extended by get-
ting through tailσ (Q).
Regarding completeness, a tableau can guide the algorithm (i) to choose valid star-
types, (ii) to ensure that δ(σ) = 1 for each nominal star-type σ, and (iii) to detect a pair
(Θ1 , Θk ) of blocking and blocked cycles as soon as each concept of the form ∃Q⊕ .D
in Θ1 is satisfied. We refer the readers to [14] for a complete proof of Lemma 1.
The following theorem is a consequence of Lemma 1.
Theorem 1. SHOIQ(+) is decidable.
4 Conclusion
In this paper, we have presented a decision procedure for the description logic SHOIQ
with transitive closure of roles in concept axioms, whose decidability was not known.
The most significant feature of our contribution is to introduce a structure for charac-
terizing models which have an infinite non-tree-like part. This structure would provide
an insight into regularity of such models which would be enjoyed by a more expressive
DL, such as ZOIQ [6], whose decidability remains open. In future work, we aim to
improve the algorithm by making it more goal-directed and aim to investigate another
open question about the hardness of SHOIQ(+) .
References
1. Patel-Schneider, P., Hayes, P., Horrocks, I.: OWL web ontology language semantics and
abstract syntax. In: W3C Recommendation. (2004)
2. Tobies, S.: The complexity of reasoning with cardinality restrictions and nominals in expres-
sive description logics. Journal of Artificial Intelligence Research 12 (2000) 199–217
3. Aho, A.V., Ullman, J.D.: Universality of data retrieval languages. In: Proceedings of the 6th
of ACM Symposium on Principles of Programming Language. (1979)
4. Baader, F.: Augmenting concept languages by transitive closure of roles: An alternative
to terminological cycles. In: Proceedings of the Twelfth International Joint Conference on
Artificial Intelligence. (1991)
5. Ortiz, M.: An automata-based algorithm for description logics around SRIQ. In: Proceed-
ings of the fourth Latin American Workshop on Non-Monotonic Reasoning 2008, CEUR-
WS.org (2008)
6. Calvanese, D., Eiter, T., Ortiz, M.: Regular path queries in expressive description logics with
nominals. In: IJCAI. (2009) 714–720
7. Horrocks, I., Sattler, U.: A tableau decision procedure for SHOIQ. Journal Of Automated
Reasoning 39(3) (2007) 249–276
8. Motik, B., Shearer, R., Horrocks, I.: Hypertableau reasoning for description logics. J. of
Artificial Intelligence Research 36 (2009) 165–228
9. Pratt-Hartmann, I.: Complexity of the two-variable fragment with counting quantifiers. Jour-
nal of Logic, Language and Information 14(3) (2005) 369–395
10. Le Duc, C., Lamolle, M.: Decidability of description logics with transitive closure of
roles. In: Proceedings of the 23rd International Workshop on Description Logics (DL 2010),
CEUR-WS.org (2010)
11. Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for expressive description logics.
In: Proceedings of the International Conference on Logic for Programming, Artificial Intel-
ligence and Reasoning (LPAR 1999), Springer (1999)
12. Baader, F., Nutt, W.: Basic description logics. In: The Description Logic Handbook: Theory,
Implementation and Applications (2nd edition), Cambridge University Press (2007) 47–104
13. Fischer, M.J., Ladner, R.I.: Propositional dynamic logic of regular programs. Journal of
Computer and System Sciences 18(18) (1979) 174–211
14. Le Duc, C., Lamolle, M., Curé, O.: A decision procedure for SHOIQ with tran-
sitive closure of roles in concept axioms. In: Technical Report, http://www.iut.univ-
paris8.fr/∼leduc/papers/RR-SHOIQTr.pdf (2013)