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 application 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.
The ontology language OWL-DL [
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 [
In the DL literature ([
f g must have two distinct paths from x to the individual satisfying nominal o. Intuitively, we can see that (i) such a x must satisfy 9S+:fog 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.
This example shows that methods ([
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
[
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 allows us to represent a model of a SHOIQ(+) knowledge base. 3 This example is initially proposed by Sebastian Rudolph from an informal discussion
sitive role names. We use RI = fP j P 2 Rg to denote a set of inverse roles, and R = fQ+ j Q 2 R [ RIg 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 2= R and S 2= 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
R I = fhx; yi 2 I I j hy; xi 2 RI g for all R 2 R, hx; zi 2 SI ; hz; yi 2 SI implies hx; yi 2 SI for each S 2 R+, and
(Q+)I = [ (Qn)I with (Q1)I = QI , (Qn)I = fhx; yi 2 ( I )2 j 9z 2 n>0
I ; hx; zi 2 (Qn 1)I ; hz; yi 2 QI g for Q+ 2 R
An interpretation I satisfies a role hierarchy R if RI SI for each R v S 2 R. Such an interpretation is called a model of R, denoted by I j= R. To simplify notations for nested inverse roles and transitive closures of roles, we define two functions and as follows: R = >:><>8> (SSRS+ )+ iiiiffff RRRR 2=== R(SSS+;,a)Sn+d2,SSR22; RR; R = >:>><>8 ((SRSS++ ))++ iiiiffff RRRR 2=== R((SSS;++a))n+daaSnndd2SSR22; RR;
A relation v is defined as the transitive-reflexive closure R+ of v on R [ fR v S j R v S 2 Rg [ fR v S j R v S 2 Rg [ fQ v Q j Q 2 R [ RIg. We define a function Trans(R) which returns true iff there is some Q 2 R+ [ fP j P 2 R+g [ fP j P 2 R [ RIg such that QvR 2 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 [
Definition 2 (terminology). Let C be a non-empty set of concept names with a nonempty 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, 9R:C, 8R: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 = CI \ DI , (C tD)I = CI [DI , (:C)I = I nCI , jfoI gj = 1 for all o 2 Co, (9R:C)I = fx 2
I j 9y 2 I ; hx; yi 2 RI ^ y 2 CI g, (8R:C)I = fx 2 I j 8y 2 I ; hx; yi 2 RI ) y 2 CI g, ( n S:C)I = fx 2 I j jfy 2 CI j hx; yi 2 SI j ng, ( n S:C)I = fx 2 I j jfy 2 CI j hx; yi 2 SI j ng where jSj 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 CI 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 j= 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 j= T and I j= R. A concept C is called satisfiable w.r.t. (T ; R) iff there is some interpretation I such that I j= R, I j= T and CI 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 CI 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
equivalences as presented in [
For a generating concept ( nS:C) and a set I f0; ; log n + 1g, we denote C(I nS:C) = l C(i nS:C) u l :C(j nS:C) where C(i nS:C) are new concept names for 0
i cl2(T ; R) = fC(i S:C) j (
i2I j2=I
log n + 1. We define cl2(T ; R) as follows:
nS:C) 2 cl(T ; R) [ cl1(T ; R); 0
i
log n + 1g[
fC(I nS:C) j (
nS:C) 2 cl(T ; R) [ cl1(T ; R); I
f0; ; log n + 1gg
Remark 1. If numbers are encoded in binary then the number of new concept names
C(i nS:D) for 0 i log n + 1, is bounded by O(j(T ; R)j) since n is bounded by
O(2j(T ;R)j). This implies that jcl2(T ; R)j is bounded by O(2j(T ;R)j). Note that two
concepts C(I nS:C) and C(J nS:C) are disjoint for all I; J f0; ; log n + 1g, I 6= J .
The concepts C(9S:C) and C(I nS:C) 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 [
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 [
This section starts by translating star-type and frame structures presented by PrattHartmann (2005) for C2 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 ( ) 2 2CL(T ;R) is called core label, ( ) = (hr1; l1i; ; hrd; ldi) is a d-tuple over 2R(T ;R) 2CL(T ;R). A pair hr; li is a ray of if hr; li = hri; lii 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 2 ( ) for some o 2 Co. – A star-type is chromatic if 6= 0 implies l( ) 6= l( 0) for two rays ; 0 of .
– 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( ).
for the set of all star-types for (T ; R).
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 2 T then nnf(:C t D) 2 ( ); 2. fA; :Ag 6 for every concept name A where = ( ) or = l( ) for each 2 ( ); 3. If C1 u C2 2 ( ) then fC1; C2g ( ); 4. If C1 t C2 2 ( ) then fC1; C2g \ ( ) 6= ;; 5. If 9R:C 2 ( ) then there is some ray 2 ( ) such that C 2 l( ) and R 2 r( ); 6. If ( nS:C) 2 ( ) and there is some ray 2 ( ) such that S 2 r( ) then
C 2 l( ) or :_C 2 l( ); 7. If ( nS:C) 2 ( ) and there is some ray 2 ( ) such that C 2 l( ) and S 2 r( ) then there is some 1 m n such that f( mS:C); ( mS:C)g ( ); 8. For each ray 2 ( ), if R 2 r( ) and RvS then S 2 r( ); C ( ) and R 2 r( ) for some ray 2 ( ) then C 2 l( );
( ), SvR, Trans(S) and R 2 r( ) for some ray 9. If 8R:C 2 10. If 8R:D 2
8S:D 2 l( ); 11. If 8Q :C 2 ( ), RvQ and R 2 r( ) for some ray 12. If 9Q :C 2 ( ) then (9Q:C t 9Q:9Q :C) 2 ( ); 13. If ( nS:C) 2 ( ) then there are n distinct rays 1; ; n 2 fC; C(Ii nS:C)g l( i), S 2 r( i) for all 1 i n; and Ij ; Ik 1g, Ij 6= Ik for all 1 j < k n. 14. If ( nS:C) 2 ( ) and there do not exist n + 1 rays 0;
C 2 l( i) and S 2 r( i) for all 0 i n. 2 ( ) then 8Q :C 2 l( );
( ) such that f0; ; log n + ; n 2 ( ) such that
C ( ) then
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); i 2 ( i) and di 2 N for 1 i k.
; ( k; k; dk)i a sequence where i 2 – tail(P) = ( k; k; dk), tail (P) = k, tail (P) = k, tail (P) = dk and jPj = 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 2 N ; 2. No N is a set of nominal star-types; 3. is a function that maps each pair ( ; ) with 2 N and 2 ( ) to a sequence ( ; ) = h( 1; 1; d1); ; ( m; m; dm)i with i 2 N , i 2 ( i), di 2 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 ( ) = fR j R 2 r( )g. 4. is a function : N ! N. By abuse of notation, we also use to denote a function which maps each pair ( ; ) with 2 N and 2 ( ) into a number in N, i.e., ( ; ) 2 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 2 ( ), a list ( ; ) of triples ( i; i; di) with i 2 ( i) is maintained where i is a “neighbor” star-type of via 2 ( ), 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:
We define P P0 if tail (P) = tail (P0) and tail (P) = tail (P0). Since is an equivalence relation over the set of all paths, we use P to denote the set of all equivalence classes [P] of paths in F . For [P]; [Q] 2 P, we define: 1. [P] is a neighbor ( 0-neighbor) of [Q] if there are P0 2 [P] and Q0 2 [Q] such that
Q0 is a neighbor ( 0-neighbor) of P0; 2. [Q] is a reachable path of [P] if there are [P1]; ; [Pn] 2 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 P0 2 [P] and Q0 2 [Q] such that Q0 is a
Q-neighbor of P0, or P0 is a Q -neighbor of Q0; 4. [Q] is a Q-reachable path of [P] if there are [P1]; ; [Pn] 2 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; P0 with tail (P) 6= tail (P0), we have P P0 if tail (P) = tail (P0) and tail (P) = tail (P0). 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 2 P and 2 (tail (P)) such that for each (P; ; Q) 2 the following conditions are satisfied: (a) tail (P) > 1 and tail (Q) > 1; (b) If P0 is the -neighbor of P then tail (P0) = tail (Q); (c) for each sequence P1; ; Pn 2 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 (P00; 00; Q00) 2 such that i. either Q00 = Pj , tail (Pj+1) = tail (P00), tail (Pj+1) tail (P00) and
Pj is the -neighbor of Pj+1 for some 1 < j < n, ii. or there are Pn+1; ; Pn+m 2 P with Q00 = Pn+m 1, tail (Pn+m) = tail (P00), tail (Pn+m) tail (P00) 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) 2 and for each sequence
P1; ; Pn 2 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 (P00; 00; Q00) 2 0 such that
(a) either Q00 = Pj , tail (Pj+1) = tail (P00), tail (Pj+1) tail (P00) and Pj is
a -neighbor of Pj+1 for some 1 < j < n,
(b) or there are Pn+1; ; Pn+m 2 P with Q00 = Pn+m 1, tail (Pn+m) =
tail (P00), tail (Pn+m) tail (P00) 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 (P00) holds in
Conditions 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) 2 goes through a star-type
= tail (Q0) with some (P0; 0; Q0) 2 . Such a cycle, which is similar to
blockingblocked nodes in completion graphs for SHOIQ [
Definition 8 (blocking). Let F = hN ; No; ; i be a frame for a SHOIQ(+) knowledge base (T ; R) with a set P of all paths in F .
each (P0; 0; Q0) 2 0 there is some (P; ; Q) 2 such that L(P) = L(P0), 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) 2 2CL(T ;R) 2R(T ;R) 2CL(T ;R) with 9Q :D 2 , – if there is some path Pk with (Pk; k; Qk) 2 k, L(Pk) = , L(Qk) = 0, s = r( k) such that Pk has no Q-reachable path Pk0 with 9Q:D 2 L(Pk0), – then there is some P1 with (P1; 1; Q1) 2 1, L(P1) = , L(Q1) = 0, r( 1) = s such that for each 9P :C 2 L(P1), there is a P -reachable path Q00 of P1 with 9P:C 2 L(Q00), and there are two triples (Pj ; j ; Qj ) 2 j and (Pj+1; j+1; Qj+1) 2 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) 2 k and L(P) contains concepts of the form 9Q :D which are not satisfied by reachable paths of P then there exists some P0 with (P0; 0; Q0) 2 1 which allows for satisfying these concepts 9Q :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) 2 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:
P0. 1. For each o 2 Co there is a unique o 2 No such that o 2 ( o) and ( o) = 1; 2. For each 2 N , is valid; 3. If 9Q :C 2 (tail (P0)) for some P0 2 P then there are P; P0 2 P such that one of the following conditions is satisfied: (a) P0 = P = P0 and 9Q:C 2 L(P0); (b) P0 is a Q-reachable of P, and 9Q:C 2 L(P0) where P = P0 or P blocks P0; (c) P is a Q -reachable of P0, and 9Q:C 2 L(P0) where P = P0 or P blocks C
Conditions 1-3 in Definition 9 ensure satisfaction of tableau properties [
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 2 (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( )[
Figure 2 depicts a frame when executing Algorithm 1 for K1 in the example presented in Section 1. The algorithm builds a frame F = hN ; No; ; i where N = f 0; 1; 2; 3; 4g and No = f 0g. The dashed arrows indicate how the function ( ; ) can be built. For example, ( 0; 0) = f( 1; 0; 1)g, ( 0; 1) = f( 2; 00; 1)g 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 indicates 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 “label” of x contains 9Q+:fog, there is a path containing S which goes back the individual satisfying 0. Thus, the concept 9Q+:fog is satisfied for each individual whose label contains 9Q+:fog.
Lemma 1. Let (T ; R) be a SHOIQ(+) knowledge base.
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 fog; A
R0
number of different star-types is bounded; (ii) the detection of a blocked cycle
according to Definition 8 terminates. For the soundness of Algorithm 1, we can extend the set
P of paths to a set Pcof extended paths by “unravelling” the frame between
blockingblocked cycles. A tableau [
Regarding completeness, a tableau can guide the algorithm (i) to choose valid
startypes, (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 9Q :D
in 1 is satisfied. We refer the readers to [
Theorem 1. SHOIQ(+) is decidable. 4
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
characterizing 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 [