A Technique for Handling the Right Hand Side of Complex RIAs

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 R v_Q P .

Keywords

• Description Logic
• Manufacturing system
• Tableau

Introduction

Description Logics [ 1 ] are a well-established branch of logics for knowledge representation 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 Ontology 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 nite 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 strati ed 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 individual 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, re exive, symmetric, transitive, and irre exive roles, disjoint roles, and the construct 9R: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 de ne a new role (P ; x) that remembers in which object is related to the role. We de ne 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 nally, set of simple role names NS NR. The set of roles is NR [ fR jR 2 NRg. According to [ 6 ], syntax and semantics of the RIQ DL concepts are given in de nitions 1 and 2.

De nition 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, 8R:C, 9R:C, ( nS:C), ( nS:C) are concepts. tu The semantics of the RIQ DL is de ned by using interpretation. An interpretation 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 CI I ; every role name R with a binary relation RI I I [ 6 ]. De nition 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 = fhx; yi : hy; xi 2 RI g, { If R1, R2,. . . , Rn are roles then (R1R2 : : : 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 nonnegative integer, then 3 3 ]M denotes cardinality of set M . >I = I ; ?I = ;; (:C)I = I nCI ; (C u D)I = CI \ DI ; (C t D)I = CI [ DI ; (9R:C)I = fx : 9y: hx; yi 2 RI ^ y 2 CI g; (8R:C)I = fx : 8y: hx; yi 2 RI ) y 2 CI g; ( nS:C)I = fx : ]fy : hx; yi 2 SI ^ y 2 CI g ng; ( nS:C)I = fx : ]fy : hx; yi 2 SI ^ y 2 CI g ng.

Number restrictions ( nS:C) and ( nS:C), are restricted to simple roles, in order to have RIQ decidability. tu

Strict partial order (irre exive, 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 2. R 2 NRnNS is a role name and (a) w = RR, or (b) w = R , or (c) w = S1 Sn and Si R, for 1 (d) w = RS1 Sn and Si R, for 1 (e) w = S1 SnR and Si R, for 1 i i i n, or n, or n.

R is a simple role, Note that the notion of simple role has the same meaning as de ned 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 nite 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 satis es a RIA S1 Snv_ R, if S1I SnI RI . A RIQ concept C is satis able w.r.t. RBox R if there is an interpretation I such that CI 6= ; and I satis es all RIA in R [ 6, 11 ]. In this paper we extend regular RIQ-RBox with one RIA of the form w v_Q

P (1) where w = S1 S2 Sn, Si Q, P Q and there is no i, such that P Si. An interpretation I satis es a RIA of the form w v_Q P , if wI QI P I . In the rest of the paper we check satis ability of concept C0 w.r.t. de ned RBox R and de ne RC0 = fRjR is role that occurs in C0 or Rg. 3

The simple reduction and general idea

Lemma 1. Let C0 be RIQ concepts and R regular RBox with a RIA of the form w v_QP , where F un(P ) holds. Let U be a new role name. We de ne

C1 := 8U:(8w:(9P :>)) u 8w:(9P :>); and set

R1 := Rnfwv_ QP g [ fU U v_ U; U v_ U g [ fRv_ U jR 2 RC0 g [ fwP v_ Qg:

Then, RIQ concept C0 is satis able w.r.t. RBox R i concept C0 u C1 is satis able w.r.t. Rbox R1.

Proof. The proof is based on transformation from one interpretation to another one. tu Without restriction F un(P ), lemma (1) do not holds. It is illustrated in example (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 heel and crankshaf tInEngine are part-of relations [ 2 ]. The model corresponds to next RIA of the form [ 13 ]: engineInCar crankshaf tInEngine powers v_wheelInCar hubInW heel (2) Let I be an interpretation, shown on Figure (1b), of the RIA of the form (2). The interpretation I satis es 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. tu (a) 4 The Uni ed Modeling Language (http://www.uml.org/) x0 x1

w hubInWheel wheelInCar w

wheelInCar z0 (b) hubInWheel y0 y1

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; y1i 2 (hubInW heel )I corresponds to object y0, while hz0; x1i 2 (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 de ned. The role satis es (R; x)v_ R: (3) For example, in case of the interpretation, shown on Figure (1b), one can dene new roles, as follows: (hubInW heel ; x0), (hubInW heel ; y0), which satisfy hz0; x1i 2 (hubInW heel ; x0)I, hz0; y1i 2 (hubInW heel ; y0)I, but hz0; x1i 2= (hubInW heel ; y0)I. Now, one can de ne new tableau concept (constructor) denoted as 9 (hubInW heel ; x):D. This constructor is used in the label of nodes 8 of the tableau (see de nition 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 = fDj 9 (hubInW heel ; x0):D 2 L(z0)g = fDj8wheelInCar:D 2 L(x0)g 6= ; 8 then there exists x1 such that hz0; x1i 2 E((hubInW heel ; x0)) and Z L(x1). 4

The extension of RI Q tableau This section examines how to extend tableau for the RIQ DL with the new constructor. We denote, as de ned 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, Bq 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 de ned as follows: f clos(C0; R) = clos(C0) [ f8BRq:Dj8R:D 2 clos(C0) and q is a state in BRg; ef c(C0; R; S) = f clos(C0; R) [ f8Bwq: 98 (P ; s):Djs 2 S; 8Q:D 2 clos(C0)g [ f 98 (P ; s):Djs 2 S; 8Q:D 2 clos(C0)g: Let's denote

P L(Bw) = hw0; qi jq is a state in Bw; (8w00 2 L(Bwq)) w0w00 2 L(Bw) : De nition 3. T=(S, L, E) is tableau for concept C0 w.r.t. R i 5 { S is non-empty set, { L : S ! 2efc(C0;R;S), { E : RC0 [ f(P ; s)js 2 Sg ! 2S S { C0 2 L(s) for some s 2 S 5 w, Q and P refer to the RIA axiom of the form w v_Q P: Next, s; t 2 S; C; C1; C2 2 f clos(C0;R); R; S 2 RC0 and ST (s; C) [ 5 ] satis es rules (P1a), (P1b), (P2), (P3), (P4a), (P4b), (P5), (P6), (P7), (P8), (P9), (P10), (P13) de ned in [ 5 ], and satis es new rules: { (P6b) If 8Q:C 2 L(s), then 8Bw: 89 (P ; s):C 2 L(s). { (P15a) 8Q:> 2 L(s) for all s 2 S. { (P15b) If 9 (P ; s):C1 2 L(v), then there exists t with hv; ti 2 E(P ; s) and 8 C1 2 L(t). Also, for all C2 2 f clos(C0), if 9 (P ; s):C2 8 2 L(v) then C2 2 L(t).

{ (P15c) If hv; ti 2 E(P ; s), then hv; ti 2 E(P ). tu Theorem 1. Concept C0 is satis able w.r.t. R i there exists tableau for C0 w.r.t. R.

De nition 4. (Completion tree) Completion tree for C0 w.r.t R is labelled tree G = (V; E; L; 6 =_) where each node x 2 V is labelled with a set L(x) ef c(C0; R; V ) [ f mR:Cj nR:C 2 clos(C0); m ng. Each edge hx; yi 2 E is labelled with a set L hx; yi RC0 [ f(P ; s)js 2 V g. Additionally, we care of inequalities between nodes in V , of the tree G, with a symmetric binary relation 6 =_.

If hx; yi 2 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 2 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 2 RC0 , x 2 V , C 2 clos(C0) we de ne set SG(x; C) = fyjy is S neighbour of x and C 2 L(y)g tu De nition 5. A tree G is said to contain a clash if there is a node x such that: { ? 2 L(x), or { for a concept name A, fA; :Ag L(x), or { there exists a concept ( nS:C) 2 L(x) and fy0; : : : ; yng 2 SG(x; C) with yi6 =_yj for all 0 i < j n. tu In order to provide termination of the algorithm, in [ 6 ] blocking techniques are used, and fact that the set of nodes' labels is nite. In our tableau de nition (3), if S is in nite set then ef c(C0; R; S) is also in nite. So, number of di erent L(s) is in nite. Also, sets L(s) can be in nite. To ensure that sets L(s) are nite, we de ne additional restriction on the set of RIA of the form w v_Q P . Let's suppose that language L(Bw) is nite.

If 8Bwq: 98 (P ; s):C 2 L(t) then there exists (w0; q) 2 P L(Bw) and (s; t) 2 E (w0). If n = ]f clos(C0; R), l = maxflen(w0)j(9q)(w0; q) 2 P L(Bw)g and number of successors is less than m (di erent 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) = fRg.

De nition 6. Let G = (V; E; L; 6=_ ) be completion tree and f : V function. ! V is a 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 nite, then l, ]P L(Bw) are also nite.

{ f (x) = y, { L(x) \ f clos(C0; R) = L(y) \ f clos(C0; R), { R 2 L(hz; xi) , R 2 L(hf (z); yi), { 9 (P ; f (z)):C 2 L(y).

; z):C 2 L(x) , 89m(Patch with L(hu; vi), denoted with L(hx; yi) 2. We 8say that L(hx; yi) f

L(hu; vi), if { L(hx; yi) \ RC0 = L(hu; vi) \ RC0 , { (8s 2 V )((P ; s) 2 L(hx; yi) , (P ; f (s)) 2 L(hu; vi)).

De nition 7. (Blocking) A node x is label blocked if there is a function f : V ! V and there are predecessors x0; y; y0 of the node x, such that { x0 6= y, { x is successor of x0 and y is successor of y0, { L(x) f L(y), L(x0) f L(y0), { L(hx; x0i) f L(hy; y0i).

In this case we say that y blocks x. f tu tu A node is blocked if it is label blocked or its predecessor is blocked. If the predecessor 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 y0 and ( nite number of) R-neighbours of these four nodes. For the nodes, function f can be nondeterministically de ned and check the rules in the de nition (7). It is also possible to check the rules algorithmically, because the rules use only nite sets.

The non-deterministic tableau algorithm can be described as follows: { Input: Concept C0 and RBox R, { Output: "Yes" if concept C0 is satis able w.r.t. RBox R, otherwise "No" { Method: 1. step: Construct tree G = (V; E; L; 6=_ ), where V = fx0g, E = ;, L(x0) = fC0g. 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" i there exists tableau of the concept

C0 w.r.t R.

Proof. (a) 9-rule and -rule generate nite number of successors of node x. So, the set L(x) is nite and the number of (P ; y)-successors of node x is nite. There is limited number the possible labels of pairs (x0; x) 2 E that will lead the blocking of tree nodes. It means, the tree generated by the algorithm is nite. 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 nite number of expansion rules. u-rule: t-rule: 9-rule: 81-rule: 82-rule: 83-rule: then L(y) ! L(y) [ f8Bq:Cg If 8B:C 2 L(x), x is not indirectly blocked,

" 2 L(B) and C 2= L(x) then L(x) ! L(x) [ fCg If 8Q:C 2 L(x), x is not indirectly blocked, and

; x):C 2= L(x) For such a path, we de ne 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 de ned inductively, as follows: { If x0 2 V is the root of tree then hx0; x0i 2 P aths(G), { If p 2 P aths(G) and z 2 V and z is not indirectly blocked, such that hT ail(p); zi 2 E, then hp; (G(z; z); z)i 2 P aths(G).

Let's de ne structure T = fS; L0; Eg as follows: S = P aths(G), E(S) = fhp; qi 2 P aths(G) P aths(G)jq = hp; (G(z; z); z)i and S 2 L(hT ail(p); zi) or p = hq; (G(z; z); z)i and Inv(S) 2 L(hT ail(q); zi)g, for S 2 RC0 , E(P ; r) = fhp; qi 2 E(P )j hr; pi 2 E(R) and (P ; G(T ail0(p); T ail0(r))) 2 L(G(T ail0(p); T ail0(p)); T ail0(q))g, L0(p) = L(T ail(p)) \ f clos(C0; R) [ f8R: 9 (P ; p):Cj8Q:C 2 L(T ail(p))g [ 8 f 98 (P ; r):Cj hr; pi 2 E(R) and 9 (P ; T ail0(r)):C 2 L(T ail0(p))g.

Let's prove that T is tableau8 for C0 w.r.t R. We consider only (P15b) property, and avoid already de ned properties in [ 6 ]. New properties (P6b), (P15a), (P15c) imply from 84, 85 and ( 89 )1.

Suppose 9 (P ; r):C 2 L0(p) then hr; pi 2 E(R) and 9 (P ; T ail0(r)):C 2 L(T ail0(p)). B8ecause of hr; pi 2 E(R), four cases are possible: 8 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 2 E(R) blocking de nition we have R 2 L(hT ail(r); zi) and R 2 L(G(z; T ail(r)); G(z; z)), while, from 9 (P ; T ail0(r)):C 2 L(z) we have 9 (P ; G(z; T ail(r)):C 2 L(G(z; z)). Ac8 8 cording to the rule ( 89 )1, we have that there exists node y such that P ; (P ; G(z; T ail(r)) 2 L(hG(z; z); yi). Let q = hp; (G(y; y); y)i then hp; qi 2 E(P ) and (P ; G(T ail0(p); T ail0(r))) 2 L(G(T ail0(p); T ail0(p)); T ail0(q)), so hp; qi 2 E(P ; r). Having regard to the rule ( 98 )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).

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 S1S2 Snv_ R1R2 Rm, with restriction that corresponding languages are nite. 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 w v_QP when the language L(Bw) is in nite.

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 Collaborative 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 Representation and Reasoning (KR 2006 ). pages 57 - 67 , 2006 .

6. I. Horrocks , U. Sattler . Decidability of SHIQ with Complex Role Inclusion Axioms . Arti cial 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 Arti cial 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 Description 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 Automated Reasoning (IJCAR 2010 ). pages 472 - 487 , Edinburgh, UK, 2010 .

13. N. Krdzavac , 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 .