=Paper=
{{Paper
|id=None
|storemode=property
|title=A Technique for Handling the Right Hand Side of Complex RIAs
|pdfUrl=https://ceur-ws.org/Vol-745/paper_34.pdf
|volume=Vol-745
|dblpUrl=https://dblp.org/rec/conf/dlog/MosurovicK11
}}
==A Technique for Handling the Right Hand Side of Complex RIAs==
https://ceur-ws.org/Vol-745/paper_34.pdf
A Technique for Handling the Right Hand Side
of Complex RIAs
Milenko Mosurović1 and Nenad Krdžavac2
1
Faculty of Mathematics and Natural Science,
University of Montenegro, Podgorica,
ul. Džordža Vašingtona bb, 81000 Podgorica, Montenegro
2
School of Electrical and Computer Engineering of Applied Studies in Belgrade,
University of Belgrade, Serbia,
ul. Vojvode Stepe 283, 11000 Belgrade, Serbia
Abstract. This paper examines a new technique based on tableau, that
allows one to introduce composition of roles from the right hand side
of complex role inclusion axioms (RIAs). Our motivation comes from
modeling product models in manufacturing systems. The series of papers,
so far, have studied the extension of tableau algorithm for Description
Logics (DLs) to capture complex RIAs. However, such RIAs permit only
the left hand side of the composition of roles. To illustrate the technique,
we extend RIQ DL with one RIA of the form Rv̇Q ◦ P .
Keywords: Description Logic, Manufacturing system,Tableau.
1 Introduction
Description Logics [1] are a well-established branch of logics for knowledge rep-
resentation and reasoning about it. Recent research in DLs has usually focused
on the logics of the so-called SH family as basis for the standard Web Ontol-
ogy Languages (OWL) [10]. In particular, the DL SHIQ [8] is closely related
to OWL-Lite and extends the basic ALC [1](the minimal propositionally closed
DL) with inverse roles and number restrictions, as well as with role inclusions
and transitive roles. The DL known as SHOIQ [7], underlying OWL-DL, further
extends SHIQ with nominals. Logics, SHIQ and SHOIQ were enhanced with
regular role hierarchies in which the composition of a chain of roles may imply
another role. These and other features were included in their extensions known
as SRIQ [9] and SROIQ [5] respectively; the latter underlies the new OWL 2
[4] standard. For reasoning in them, the adaptations of the tableaux algorithms
were proposed [9, 5]. In a pre-processing stage, the implications between roles,
given by the role hierarchy, are captured in a set of non-deterministic finite state
automata (NFA). The complexity of these logics is studied in [11]. Also, there
exists another extensions of the logics with description graphs [14] and stratified
ontologies [12]. Motivation for our research is based on modeling product models
in manufacturing systems (see UML model on Figure 1) [3]. For example, when
an individual crankshaft in individual engine in an individual car, powers indi-
vidual hubs in individual wheels in the same car, and not the hubs in the wheels
in the other cars [13]. Such modeling example can be represented as RIAs with
more then one role on the right hand side of role composition [13]. The aim of this
paper is to show a technique that can allow the extension of RIQ DL [6] with a
RIA of the form Rv̇Q ◦ P . The RIQ DL [6], is the fragment of SRIQ (without
Abox, as well as, reflexive, symmetric, transitive, and irreflexive roles, disjoint
roles, and the construct ∃R.Self ) [9]. To avoid analysis of restrictions that roles
must satisfy in new RIAs, we consider only one RIA of the form Rv̇Q ◦ P . Main
idea is to define a new role (P − , x) that remembers in which object is related to
the role. We define new constructor which will deal with these roles.
The paper is organized as follows. Next section gives short overview of RIQ DL
and its role hierarchy. Section (3) explains simple reduction problem and gives
general idea. Section (4), outlines the extension of RIQ tableau, while section
(5) gives formal proof of the correctness and termination of tableau algorithm.
Finaly we give some remarks and explane future work.
2 Preliminaries
This section, in brief, outlines syntax and semantics of RIQ DL and regular role
hierarchy. The alphabet of RIQ DL consists of set of concept names NC , set of
role names NR and finally, set of simple role names NS ⊂ NR . The set of roles
is NR ∪ {R− |R ∈ NR }. According to [6], syntax and semantics of the RIQ DL
concepts are given in definitions 1 and 2.
Definition 1. Set of RIQ concepts is a smallest set such that
– every concept name and >, ⊥ are concepts, and,
– if C and D are concept and R is a role, S is simple role, n is non-negative
integer, then ¬C, C u D, C t D, ∀R.C, ∃R.C, (≤ nS.C), (≥ nS.C) are
concepts. t
u
The semantics of the RIQ DL is defined by using interpretation. An interpre-
tation is a pair I = (∆I , ·I ), where ∆I is a non-empty set, called the domain
of the interpretation. A valuation ·I associates: every concept name C with a
subset C I ⊆ ∆I ; every role name R with a binary relation RI ⊆ ∆I × ∆I [6].
Definition 2. An interpretation I extends to RIQ complex concepts and roles
according to the following semantic rules:
– If R is a role name, then (R− )I = {hx, yi : hy, xi ∈ RI },
– If R1 , R2 ,. . . , Rn are roles then (R1 R2 . . . Rn )I = (R1 )I ◦(R2 )I ◦· · ·◦(Rn )I ,
where sign ◦ is a composition of binary relations,
– If C and D are concepts, R is a role, S is a simple role and n is a non-
negative integer, then 3
3
]M denotes cardinality of set M .
>I = ∆I , ⊥I = ∅, (¬C)I = ∆I \C I ,
(C u D)I = C I ∩ DI , (C t D)I = C I ∪ DI ,
(∃R.C)I = {x : ∃y. hx, yi ∈ RI ∧ y ∈ C I },
(∀R.C)I = {x : ∀y. hx, yi ∈ RI ⇒ y ∈ C I },
(≥ nS.C)I = {x : ]{y : hx, yi ∈ S I ∧ y ∈ C I } ≥ n},
(≤ nS.C)I = {x : ]{y : hx, yi ∈ S I ∧ y ∈ C I } ≤ n}.
Number restrictions (≥ nS.C) and (≤ nS.C), are restricted to simple roles, in
order to have RIQ decidability. t
u
Strict partial order ≺ (irreflexive, transitive, and antisymmetric), on the set
of roles, provides acyclicity [6]. Allowed RIAs in RIQ DL with respect to ≺, are
expressions of the form wv̇R, where [6]:
1. R is a simple role name, w = S and S ≺ R is a simple role,
2. R ∈ NR \NS is a role name and
(a) w = RR, or
(b) w = R− , or
(c) w = S1 · · · Sn and Si ≺ R, for 1 ≤ i ≤ n, or
(d) w = RS1 · · · Sn and Si ≺ R, for 1 ≤ i ≤ n, or
(e) w = S1 · · · Sn R and Si ≺ R, for 1 ≤ i ≤ n.
Note that the notion of simple role has the same meaning as defined in [5]. So,
we use the simple role S carefully in allowed RIAs to avoid R1 ◦ R2 v S.
A RIQ RBox (role hierarchy) is a finite set R of RIAs. A role hierarchy R is
regular if there exists strict partial order ≺ such that each RIA in R is regular
[6]. An interpretation I satisfies a RIA S1 · · · Sn v̇R, if S1I ◦ · · · ◦ SnI ⊆RI . A RIQ
concept C is satisfiable w.r.t. RBox R if there is an interpretation I such that
C I 6= ∅ and I satisfies all RIA in R [6, 11]. In this paper we extend regular
RIQ-RBox with one RIA of the form
wv̇Q ◦ P (1)
where w = S1 ◦ S2 · · · Sn , Si ≺ Q, P ≺ Q and there is no i, such that P ≺ Si .
An interpretation I satisfies a RIA of the form wv̇Q ◦ P , if wI ⊆ QI ◦ P I . In
the rest of the paper we check satisfiability of concept C0 w.r.t. defined RBox R
and define RC0 = {R|R is role that occurs in C0 or R}.
3 The simple reduction and general idea
Tableau algorithm in [6] tries to construct a tableau for RIQ-concept C. In pre-
processing step the role hierarchy is translated into NFA, that are used, both,
in the definition of a tableau and in the tableau algorithm. Intuitively, an au-
tomaton is used to memorize path between an object x that has to satisfy a
concept of the form ∀R.C and other objects, and then to determine which of
these objects must satisfy C [6]. Similar idea can be used in extension RIQ with
a RIA of the form wv̇Q ◦ P . If an object x should satisfies concept ∀Q.C then
we should define structure that will remember path w ◦ P − from the object x to
objects that must satisfy concept C. If we extend RIQ DL with F un [11], then
the next lemma holds:
Lemma 1. Let C0 be RIQ concepts and R regular RBox with a RIA of the
form wv̇QP , where F un(P − ) holds. Let U be a new role name. We define
C1 := ∀U.(∀w.(∃P − .>)) u ∀w.(∃P − .>),
and set
R1 := R\{wv̇QP } ∪ {U U v̇U, U − v̇U } ∪ {Rv̇U |R ∈ RC0 } ∪ {wP − v̇Q}.
Then, RIQ concept C0 is satisfiable w.r.t. RBox R iff concept C0 u C1 is
satisfiable w.r.t. Rbox R1 .
Proof. The proof is based on transformation from one interpretation to another
one. t
u
Without restriction F un(P − ), lemma (1) do not holds. It is illustrated in exam-
ple (1).
Example 1. The UML4 model of a car, shown on Figure (1a), describes Car with
following parts: Engine, W heel, Crankshaf t and Hub. Role name powers is
part-part relation [13, 2], but role names engineInCar, wheelInCar, hubInW he-
el and crankshaf tInEngine are part-of relations [2]. The model corresponds to
next RIA of the form [13]:
engineInCar ◦crankshaf tInEngine◦powersv̇wheelInCar ◦hubInW heel (2)
Let I be an interpretation, shown on Figure (1b), of the RIA of the form (2).
The interpretation I satisfies RIA of the form wv̇wheelInCar ◦ hubInW heel,
but it does not satisfy RIA of the form w ◦ hubInW heel− v̇wheelInCar, where
w = engineInCar ◦ crankshaf tInEngine ◦ powers. t
u
x0 y0
w
wheelInCar wheelInCar
w
hubInWheel
x1 z0 y1
hubInWheel
(a) (b)
Fig. 1. (a) An UML product model (updated from [13]). (b) An interpretation I of
RIA of the form (2).
4
The Unified Modeling Language (http://www.uml.org/)
According to the Figure (1b), one can conclude that the restriction problems
for reduction of RIAs is caused by the role hubInW heel− . The role is not
”unambiguously” determined. On the other side, by using the interpretation
shown on the Figure (1b), it is obvious hz0 , y1 i ∈ (hubInW heel− )I corresponds
to object y0 , while hz0 , x1 i ∈ (hubInW heel− )I corresponds to object x0 . In the
other words, the condition of existence unambiguously role is connected to an
object. To stressed which particular object corresponds to the role name, a new
role (R, x) is defined. The role satisfies
(R, x)v̇R. (3)
For example, in case of the interpretation, shown on Figure (1b), one can de-
fine new roles, as follows: (hubInW heel− , x0 ), (hubInW heel− , y0 ), which satisfy
hz0 , x1 i ∈ (hubInW heel− , x0 )I , hz0 , y1 i ∈ (hubInW heel− , y0 )I , but hz0 , x1 i ∈
/
(hubInW heel− , y0 )I . Now, one can define new tableau concept (constructor) de-
noted as ∀∃ (hubInW heel− , x).D. This constructor is used in the label of nodes
of the tableau (see definition 3). Intuitively, the constructor serves to write the
set of sub-concepts of the concept C0 which have to hold in some node, i.e. if
Z = {D| ∃∀ (hubInW heel− , x0 ).D ∈ L(z0 )} = {D|∀wheelInCar.D ∈ L(x0 )} 6= ∅
then there exists x1 such that hz0 , x1 i ∈ E((hubInW heel− , x0 )) and Z ⊆ L(x1 ).
4 The extension of RIQ tableau
This section examines how to extend tableau for the RIQ DL with the new
constructor. We denote, as defined in [6], BR as NFA that corresponds to role
R. We use a special automaton for word w, denoted with Bw . For B an NFA
and q a state of B, B q denotes the NFA obtained from B by making q the (only)
initial state of B [5]. The language recognized by NFA B is denoted by L(B).
The clos(C0 ) is the smallest set of concepts in negation normal form (NNF)
which contains C0 , that is closed under ¬˙ and sub-concepts [6]. For a set S the
f clos(C0 , R) and ef c(C0 , R, S) can be defined as follows:
q
f clos(C0 , R) = clos(C0 ) ∪ {∀BR .D|∀R.D ∈ clos(C0 ) and q is a state in BR },
q ∃
ef c(C0 , R, S) = f clos(C0 , R) ∪ {∀Bw . ∀ (P − , s).D|s ∈ S, ∀Q.D ∈ clos(C0 )} ∪
{ ∀∃ (P − , s).D|s ∈ S, ∀Q.D ∈ clos(C0 )}.
Let’s denote
P L(Bw ) = hw0 , qi |q is a state in Bw , (∀w00 ∈ L(Bw q
)) w0 w00 ∈ L(Bw ) .
Definition 3. T=(S, L, E) is tableau for concept C0 w.r.t. R iff5
– S is non-empty set,
– L : S → 2ef c(C0 ,R,S) ,
– E : RC0 ∪ {(P − , s)|s ∈ S} → 2S×S
– C0 ∈ L(s) for some s ∈ S
5
w, Q and P refer to the RIA axiom of the form wv̇Q ◦ P.
Next, s, t ∈ S; C, C1 , C2 ∈ f clos(C0 ,R); R, S ∈ RC0 and S T (s, C) [5] satisfies
rules (P1a), (P1b), (P2), (P3), (P4a), (P4b), (P5), (P6), (P7), (P8), (P9),
(P10), (P13) defined in [5], and satisfies new rules:
– (P6b) If ∀Q.C ∈ L(s), then ∀Bw . ∃∀ (P − , s).C ∈ L(s).
– (P15a) ∀Q.> ∈ L(s) for all s ∈ S.
– (P15b) If ∀∃ (P − , s).C1 ∈ L(v), then there exists t with hv, ti ∈ E(P − , s) and
C1 ∈ L(t). Also, for all C2 ∈ f clos(C0 ), if ∀∃ (P − , s).C2
∈ L(v) then C2 ∈ L(t).
– (P15c) If hv, ti ∈ E(P − , s), then hv, ti ∈ E(P − ). t
u
Theorem 1. Concept C0 is satisfiable w.r.t. R iff there exists tableau for C0
w.r.t. R.
Proof. For the if direction let T = (S, L, E) be a tableau for C0 w.r.t R. We
define interpretation I = (∆I , ·I ), with: ∆I = S, C I = {s|C ∈ L(s)}, for
concept names C in clos(C0 ), and for roles names R 6= Q and Q, we set
RI = {hs0 , sn i ∈ ∆I × ∆I | there are s1 , . . . , sn−1 with hsi , si+1 i ∈ E(Si+1 ) for
0 ≤ i ≤ n − 1 and S1 · · · Sn ∈ L(BR )},
QI = {hs0 , sn i | there are s1 , . . . , sn−1 with hsi , si+1 i ∈ E(Si+1 ) for 0 ≤ i ≤ n − 1
and S1 · · · Sn ∈ L(BQ )} ∪ {hx, yi |(∃z)(hx, zi ∈ wI and hz, yi ∈ E((P − , x)))}.
Let’s prove that I is model for C0 and R.
I is model for R. Let’s consider RIA of the form wv̇Q ◦ P . If hx, yi ∈ wI .
According to (P15a) and (P6b) then ∀Bw . ∃∀ (P − , x).> ∈ L(x) holds. Accord-
ing to (P4a), (P15b), (P15c) and definition of QI , P I we have (∃t) hy, ti ∈
E((P − , x)), hy, ti ∈ E(P − ) and hx, ti ∈ QI , and finally implies hx, yi ∈ (Q ◦ P )I .
I is model for C0 . It is enough to prove that C ∈ L(s) implies s ∈ C I for all
s ∈ S and C ∈ clos(C0 ). Let’s consider C ≡ ∀Q.D. For other cases the proof is
the same as proof in [6].
Let ∀Q.D ∈ L(s) and (s, t) ∈ QI . If ∃S1 · · · Sn−1 ∈ L(BQ ), so hsi , si+1 i ∈
E(Si+1 ), i = 0, . . . , n−1, s0 = s, sn = t, then the proof is the same as proof in [6].
In case of (∃z) hs, zi ∈ wI and hz, ti ∈ E(P − , s). Based on the definition of ω I
and (P6b) we have ∃∀ (P − , s).D ∈ L(z). According to (P15b), we have D ∈ L(t).
By induction t ∈ DI , so we have s ∈ (∀Q.D)I .
For the converse, suppose that I = (∆I , ·I ) is model for C0 w.r.t. R. Let’s define
tableau T = (S, L, E), as follows: S = ∆I , E(R) = RI , E((P − , x)) = {hy, zi ∈
S 2 | hx, yi ∈ wI , hx, zi ∈ QI , hz, yi ∈ P I }, and
L(s) = {C ∈ clos(C0 )|s ∈ C I }∪{∀BR .C|∀R.C ∈ clos(C0 ) and s ∈ (∀R.C)I }∪
q q
{∀BR .C ∈ f clos(C0 , R)| for all S1 · · · Sn ∈ L(BR ), s ∈ (∀S1 .
q
∀S2 · · · ∀Sn .C)I , and if ε ∈ L(BR ) then s ∈ C I } ∪ {∀Q.>} ∪ {∀Bw . ∀∃ (P −
q ∃
, s).C|s ∈ (∀Q.C)I } ∪ {∀Bw . ∀ (P − , t).C|(∃w0 ) hw0 , qi ∈ P L(Bw ) and ht, si ∈
∃
(w ) and t ∈ (∀Q.C) } ∪ { ∀ (P − , t).C| ht, si ∈ wI and t ∈ (∀Q.C)I }.
0 I I
Let’s prove that T is tableau for C0 w.r.t. R. We consider only new rules
(see definition 3). From definition E(P − , x) and E(P ) we prove (P15c). From
the definition of L(s) we have that (P15a) and (P6b) holds. Let’s prove rule
(P15b). Suppose that ∀∃ (P − , s).C1 ∈ L(v). From the definition of L(v) follows
hs, vi ∈ wI and s ∈ (∀Q.C)I . Because of I |= wv̇Q ◦ P we have that there
exists z such that hs, zi ∈ QI and hz, vi ∈ P I i.e. hv, zi ∈ E((P − , s)). On the
other hand, from s ∈ (∀Q.C)I and hs, zi ∈ QI follows z ∈ C1I , so C1 ∈ L(z). If
∃ − I I
∀ (P , s).C2 ∈ L(v) then s ∈ (∀Q.C2 ) , so z ∈ C2 , i.e. C2 ∈ L(z). t
u
5 Tableau algorithm
The tableau algorithm generates completion tree.
Definition 4. (Completion tree) Completion tree for C0 w.r.t R is labelled
tree G = (V, E, L, 6= ˙ ) where each node x ∈ V is labelled with a set L(x) ⊆
ef c(C0 , R, V ) ∪ {≤ mR.C| ≤ nR.C ∈ clos(C0 ), m ≤ n}. Each edge hx, yi ∈ E
is labelled with a set L hx, yi ⊆ RC0 ∪ {(P − , s)|s ∈ V }. Additionally, we care of
inequalities between nodes in V , of the tree G, with a symmetric binary relation
6=˙.
If hx, yi ∈ E, then y is called successor of the x, but x is called predecessor
of y. Ancestor is the transitive closure of predecessor, and descendant is the
transitive closure of successor. A node y is called an R-successor of a node x
if, for some R0 with R0 v∗ R, R0 ∈ L(hx, yi). A node y is called a neighbour
(R-neighbour) of a node x if y is a successor (R-successor) of x or if x is a
successor (Inv(R)-successor) of y. For S ∈ RC0 , x ∈ V , C ∈ clos(C0 ) we define
set S G (x, C) = {y|y is S − neighbour of x and C ∈ L(y)} t
u
Definition 5. A tree G is said to contain a clash if there is a node x such that:
– ⊥ ∈ L(x), or
– for a concept name A, {A, ¬A} ⊆ L(x), or
– there exists a concept (≤ nS.C) ∈ L(x) and {y0 , . . . , yn } ∈ S G (x, C) with
˙ yj for all 0 ≤ i < j ≤ n.
yi 6= t
u
In order to provide termination of the algorithm, in [6] blocking techniques are
used, and fact that the set of nodes’ labels is finite. In our tableau definition (3),
if S is infinite set then ef c(C0 , R, S) is also infinite. So, number of different L(s)
is infinite. Also, sets L(s) can be infinite. To ensure that sets L(s) are finite,
we define additional restriction on the set of RIA of the form wv̇Q ◦ P . Let’s
suppose that language L(Bw ) is finite.
q ∃
If ∀Bw . ∀ (P − , s).C ∈ L(t) then there exists (w0 , q) ∈ P L(Bw ) and (s, t) ∈
E(w ). If n = ]f clos(C0 , R), l = max{len(w0 )|(∃q)(w0 , q) ∈ P L(Bw )} and
0
number of successors is less than m (different than P − neighbours), then 6 :
]L(t) ≤ n· ml · ]P L(Bw ). To illustrate the technique in an understandable way,
we consider only special case, when L(Bw ) = {R}.
˙ ) be completion tree and f : V → V is a
Definition 6. Let G = (V, E, L, 6=
function.
1. We say that L(x) f − match with L(y), denoted as L(x) ∼f L(y), if
6
Because of L(Bw ) is finite, then l, ]P L(Bw ) are also finite.
– f (x) = y,
– L(x) ∩ f clos(C0 , R) = L(y) ∩ f clos(C0 , R),
– R ∈ L(hz, xi) ⇔ R ∈ L(hf (z), yi),
– ∀∃ (P − , z).C ∈ L(x) ⇔ ∃∀ (P − , f (z)).C ∈ L(y).
2. We say that L(hx, yi) f − match with L(hu, vi), denoted with L(hx, yi) ∼f
L(hu, vi), if
– L(hx, yi) ∩ RC0 = L(hu, vi) ∩ RC0 ,
– (∀s ∈ V )((P − , s) ∈ L(hx, yi) ⇔ (P − , f (s)) ∈ L(hu, vi)). t
u
Definition 7. (Blocking) A node x is label blocked if there is a function f :
V → V and there are predecessors x0 , y, y 0 of the node x, such that
– x0 6= y,
– x is successor of x0 and y is successor of y 0 ,
– L(x) ∼f L(y), L(x0 ) ∼f L(y 0 ),
– L(hx, x0 i) ∼f L(hy, y 0 i).
In this case we say that y blocks x. t
u
A node is blocked if it is label blocked or its predecessor is blocked. If the pre-
decessor of a node x is blocked, then we say that x is indirectly blocked [5].
There is an algorithm that checks whether a node y blocks node x. It is enough
to consider nodes x, y and their predecessors x0 and y 0 and (finite number of)
R-neighbours of these four nodes. For the nodes, function f can be nondeter-
ministically defined and check the rules in the definition (7). It is also possible
to check the rules algorithmically, because the rules use only finite sets.
The non-deterministic tableau algorithm can be described as follows:
– Input: Concept C0 and RBox R,
– Output: ”Yes” if concept C0 is satisfiable w.r.t. RBox R, otherwise ”No”
– Method:
˙ ), where V = {x0 }, E = ∅, L(x0 ) =
1. step: Construct tree G = (V, E, L, 6=
{C0 }. Go to step 2.
2. step: Apply an expansion rule (see table 1) to the tree G, while it is
possible. Otherwise, go to step 3.
3. step: If the tree does not contain clash return ”Yes”, otherwise return
”No”.
Theorem 2. 1. Tableau algorithm terminates when started with C0 and R,
2. Tableau algorithm returns answer ”Yes” iff there exists tableau of the concept
C0 w.r.t R.
Proof. (a) ∃-rule and ≥-rule generate finite number of successors of node x. So,
the set L(x) is finite and the number of (P − , y)-successors of node x is finite.
There is limited number the possible labels of pairs (x0 , x) ∈ E that will lead
the blocking of tree nodes. It means, the tree generated by the algorithm is
finite. According to [6], the rule which generates node y and remove rule ≤,
will not be applied, again. This means that the algorithm can applied only
finite number of expansion rules.
u-rule: If C1 u C2 ∈ L(x), x is not indirectly blocked,
and {C1 , C2 } * L(x),
then L(x) → L(x) ∪ {C1 , C2 }
t-rule: If C1 t C2 ∈ L(x), x is not indirectly blocked,
and {C1 , C2 } ∩ L(x) = ∅,
then L(x) → L(x) ∪ {E}, for some E ∈ {C1 , C2 }
∃-rule: If ∃S.C ∈ L(x), x is not blocked,
and x has no S-negihbour y where C ∈ L(y)
then create new node y where L(hx, yi) := {S} and L(y) := {C}
∀1 -rule: If ∀S.C ∈ L(x), x is not indirectly blocked,
and ∀BS .C ∈ / L(x)
then L(x) → L(x) ∪ {∀BS .C}
S
∀2 -rule: If ∀Bp .C ∈ L(x), x is not indirectly blocked, p → q ∈ Bp
q
and there is an S-neighbour y of x with ∀B .C ∈ / L(y)
then L(y) → L(y) ∪ {∀Bq .C}
∀3 -rule: If ∀B.C ∈ L(x), x is not indirectly blocked,
ε ∈ L(B) and C ∈ / L(x)
then L(x) → L(x) ∪ {C}
∀4 -rule: If ∀Q.C ∈ L(x), x is not indirectly blocked, and
∀Bw . ∃∀ (P − , x).C ∈/ L(x)
then L(x) → L(x) ∪ {∀Bw . ∃∀ (P − , x).C}
∀5 -rule: If ∀Q.> ∈ / L(x), x is not indirectly blocked
then L(x) → L(x) ∪ {∀Q.>}
( ∃∀ )1 -rule: If ∃
∀
(P − , x).C ∈ L(y), y is not blocked and
there is no z with (P − , x) ∈ L(hy, zi)
then create new node z with (P − , x) ∈ L(hy, zi), P − ∈ L(hy, zi)
( ∃∀ )2 -rule: If ∃
∀
(P − , x).C ∈ L(y), y is not blocked,
there is z with (P − , x) ∈ L(hy, zi) and C ∈ / L(z)
then L(z) → L(z) ∪ {C}
choose-rule: If (≤ nS.C) ∈ L(x), x is not indirectly blocked,
and there is an S-neighbour y of x {C, ¬C} ˙ ∩ L(y) = ∅
then L(y) → L(y) ∪ {E}, for some E ∈ {C, ¬C} ˙
≥-rule: If (1) (≥ nS.C) ∈ L(x), x is not blocked, and
(2) there are not n S-neighbours y1 , . . . , yn of x with
C ∈ L(yi ) and yi 6= ˙ yj for 1 ≤ i < j ≤ n,
then create n new nodes y1 , . . . yn with L(hx, yi i) = {S},
L(yi ) = {C} and yi 6= ˙ yj for 1 ≤ i < j ≤ n
≤-rule: If (1) (≤ nS.C) ∈ L(x), x is not indirectly blocked
˙ z and
(2) ]S G (x, C) > n and there are y, z ∈ S G (x, C) with not y 6=
y is not root node nor an ancestor of z
then (1) L(z) → L(z) ∪ L(y)
(2) if z is an ancestor of x,
then L(hz, xi) → L(hz, xi) ∪ Inv(L(hx, yi))
else L(hx, zi) → L(hx, zi) ∪ L(hx, yi)
(3) set u6= ˙ z, for all u with u6=˙y
(4) remove y and sub-tree below y from G
Table 1. Expansion rules for a tableau algorithm (updated from [5])
(b) For the if direction, suppose that the algorithm returns ”Yes”. It means that
the algorithm generated tree G = (V, E, L, 6= ˙ ) without clash and there are
no expansion rules (see table 1) that can be applied.
A path [5, 8] is a sequence of pairs of nodes of G of the form
p = h(x0 , x00 ), . . . , (xn , x0n )i . (4)
For such a path, we define T ail(p) = xn and T ail0 (p) = x0n . We denote the
path
(x0 , x00 ), (x1 , x01 ), . . . , (xn , x0n ), (xn+1 , x0n+1 ) . (5)
with p, (xn+1 , x0n+1 ) . If node x is label blocked then corresponding function
f is denoted with fx . The node x is blocked with node fx (x). We use function:
G(x, z) = z, if x is not blocked, or G(x, z) = fx (z), if x is blocked.
The set P aths(G) is defined inductively, as follows:
– If x0 ∈ V is the root of tree then hx0 , x0 i ∈ P aths(G),
– If p ∈ P aths(G) and z ∈ V and z is not indirectly blocked, such that
hT ail(p), zi ∈ E, then hp, (G(z, z), z)i ∈ P aths(G).
Let’s define structure T = {S, L0 , E} as follows:
S = P aths(G),
E(S) = {hp, qi ∈ P aths(G)×P aths(G)|q = hp, (G(z, z), z)i and S ∈ L(hT ail(p), zi)
or p = hq, (G(z, z), z)i and Inv(S) ∈ L(hT ail(q), zi)}, for S ∈ RC0 ,
E(P − , r) = {hp, qi ∈ E(P − )| hr, pi ∈ E(R) and (P − , G(T ail0 (p), T ail0 (r)))
∈ L(G(T ail0 (p), T ail0 (p)), T ail0 (q))},
L0 (p) = L(T ail(p)) ∩ f clos(C0 , R) ∪ {∀R. ∀∃ (P − , p).C|∀Q.C ∈ L(T ail(p))} ∪
{ ∃∀ (P − , r).C| hr, pi ∈ E(R) and ∃∀ (P − , T ail0 (r)).C ∈ L(T ail0 (p))}.
Let’s prove that T is tableau for C0 w.r.t R. We consider only (P15b) prop-
erty, and avoid already defined properties in [6]. New properties (P6b), (P15a),
(P15c) imply from ∀4 , ∀5 and ( ∀∃ )1 .
Suppose ∀∃ (P − , r).C ∈ L0 (p) then hr, pi ∈ E(R) and ∀∃ (P − , T ail0 (r)).C ∈
L(T ail0 (p)). Because of hr, pi ∈ E(R), four cases are possible:
1. p = hr, (G(z, z), z)i and G(z, z) = z
2. p = hr, (G(z, z), z)i and G(z, z) 6= z
3. r = hp, (G(z, z), z)i and G(z, z) = z
4. r = hp, (G(z, z), z)i and G(z, z) 6= z
The subcases above are analyzing on the similar way and we consider the
most complex of them i.e. case (2). The T ail0 (r) is not blocked, so T ail0 (r) =
T ail(r), while z is blocked by G(z, z). From hr, pi ∈ E(R) blocking definition
we have R ∈ L(hT ail(r), zi) and R ∈ L(G(z, T ail(r)), G(z, z)), while, from
∃ − 0 ∃ −
∀ (P , T ail (r)).C ∈ L(z) we have ∀ (P , G(z, T ail(r)).C ∈ L(G(z, z)). Ac-
cording to the rule ( ∀∃ )1 , we have that there exists node y such that
P − , (P − , G(z, T ail(r)) ∈ L(hG(z, z), yi). Let q = hp, (G(y, y), y)i then hp, qi ∈
E(P − ) and (P − , G(T ail0 (p), T ail0 (r))) ∈ L(G(T ail0 (p), T ail0 (p)), T ail0 (q)), so
hp, qi ∈ E(P − , r). Having regard to the rule ( ∀∃ )2 we conclude that property
(P15b) holds.
For the only-if direction, the proof is the same as proof in [6] (i.e., we take a
tableau and use it to steer the application of the non-deterministic rules). t
u
6 Conclusions and future works
This paper shortly examines how to handle complex RIAs with more than one
role from the right hand side of the composition of roles in RIQ DL. Although
the proof was conducted for RIA of the form Rv̇Q◦P , we can apply the technique
to RIA of the form S1 S2 · · · Sn v̇R1 R2 · · · Rm , with restriction that corresponding
languages are finite. Our future work will be focused on the problem which
conditions should satisfy role if we have more than one RIAs, to be mention
technique could be applied. Also, we will do research on RIA of the form wv̇QP
when the language L(Bw ) is infinite.
References
1. F. Baader, D. Calvanese, D. McGuinness, D. Nardi, and P. Patel-Schneider. The
Description Logic Handbook - Theory, Implementation and Application. Cambridge
University Press, second edition, 2007.
2. C. Bock. UML 2 Composition Model. Journal of Object Technology, 3(10):47-73,
2004.
3. C. Bock, X. F. Zha, H-W. Suh, J-H. Lee, Ontological Product Modeling for Col-
laborative Design, U.S. National Institute of Standards and Technology, Technical
Report NISTIR 7643, 2009.
4. B. C. Grau, I. Horrocks, B. Motik, B. Parsia, P. P. Schneider, and U. Sattler.
OWL 2: The next step for OWL. Journal of Web Semantics: Science, Services and
Agents on the World Wide Web. 6(4): 309-322, 2008.
5. I. Horrocks, O. Kutz, and U. Sattler. The Even More Irresistible SROIQ. In
Proceedings of the 10th International Conference on Principles of Knowledge Rep-
resentation and Reasoning (KR 2006). pages 57-67, 2006.
6. I. Horrocks, U. Sattler. Decidability of SHIQ with Complex Role Inclusion Ax-
ioms. Artificial Intelligence, 160(1-2):79-104, 2004.
7. I. Horrocks, U. Sattler. A Tableaux Decision Procedure for SHOIQ. Journal of
Automated Reasoning. Springer Verlag, 39(3): 245-429, 2007.
8. I. Horrocks, and U. Sattler. Optimised Reasoning for SHIQ. In Proceedings of the
15th European Conf. on Artificial Intelligence (ECAI 2002), pages 277-281, 2002.
9. I. Horrocks, O. Kutz, and U. Sattler. The irresistible SRIQ. In Proceedings of the
OWLED*05 Workshop on OWL: Experiences and Directions, 2005.
10. I. Horrocks, , P. F. Patel-Schneider, and F. van Harmelen. From SHIQ and RDF
to OWL: The Making of a Web Ontology Language. Journal of Web Semantics.
1(1):7-26, 2003.
11. Y. Kazakov. RIQ and SROIQ are Harder than SHOIQ. In Proceedings of De-
scription Logics Workshop (DL 2008), CEUR-Workshop. Vol. 353, 2008.
12. Y. Kazakov. An Extension of Complex Role Inclusion Axioms in the Description
Logic SROIQ. In Proceedings of the 5th International Joint Conference on Auto-
mated Reasoning (IJCAR 2010). pages 472-487, Edinburgh, UK, 2010.
13. N. Krdžavac, C. Bock. Reasoning in Manufacturing Part-Part Examples with OWL
2. U.S. National Institute of Standards and Technology, Technical Report NISTIR
7535, 2008.
14. B. Motik, R. Shearer, and I. Horrocks. Hypertableau Reasoning for Description
Logics. Journal of Articial Intelligence Research. 36: 165-228, 2009.