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 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 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 R ˙ 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 R ˙ 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.

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 N C , set of role names N R and finally, set of simple role names

N S ⊂ N R . The set of roles is N R ∪ {R − |R ∈ N R }.

According to [6], syntax and semantics of the RIQ DL concepts are given in definitions 1 and 2. The semantics of the RIQ DL is defined 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 C I ⊆ ∆ I ; every role name R with a binary relation

R I ⊆ ∆ 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 = { x, y : y, x ∈ R I }, -If R 1 , R 2 ,. . . , R n are roles then (R 1 R 2 . . . R n ) I = (R 1 ) I •(R 2 ) I •• • ••(R n ) 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, then3 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 w ˙ R, where [6]:

1. R is a simple role name, w = S and S ≺ R is a simple role, 2. R ∈ N R \N S is a role name and (a) w = RR, or (b) w = R − , or (c) w = S 1 • • • S n and S i ≺ R, for 1 ≤ i ≤ n, or (d) w = RS 1 • • • S n and S i ≺ R, for 1 ≤ i ≤ n, or (e) w = S 1 • • • S n R and S i ≺ 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

R 1 • R 2 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 S 1 • • • S n ˙ R, if S I 1 • • • • • S I n ⊆R I . A RIQ concept C is satisfiable w.r.t. RBox R if

there is an interpretation I such that C I = ∅ and I satisfies all RIA in R [6,11]. In this paper we extend regular RIQ-RBox with one RIA of the form

w ˙ Q • P(1)

where

w = S 1 • S 2 • • • S n , S i ≺ Q, P ≺ Q and there is no i, such that P ≺ S i . An interpretation I satisfies a RIA of the form w ˙ Q • P , if w I ⊆ Q I • P I .

In the rest of the paper we check satisfiability of concept C 0 w.r.t. defined RBox R and define R C0 = {R|R is role that occurs in C 0 or R}.

The simple reduction and general idea

Tableau algorithm in [6] tries to construct a tableau for RIQ-concept C. In preprocessing 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 automaton 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 w ˙ 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 C 0 be RIQ concepts and R regular RBox with a RIA of the form w ˙ QP , where F un(P − ) holds. Let U be a new role name. We define

C 1 := ∀U.(∀w.(∃P − . )) ∀w.(∃P − . ),

and set

R 1 := R\{w ˙ QP } ∪ {U U ˙ U, U − ˙ U } ∪ {R ˙ U |R ∈ R C0 } ∪ {wP − ˙ Q}. Then, RIQ concept C 0 is satisfiable w.r.t. RBox R iff concept C 0 C 1 is satisfiable w.r.t. Rbox R 1 .

Proof. The proof is based on transformation from one interpretation to another one.

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]: 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 z 0 , y 1 ∈ (hubInW heel − ) I corresponds to object y 0 , while z 0 , x 1 ∈ (hubInW heel − ) I corresponds to object x 0 . 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) ˙ R.

(

)3

For example, in case of the interpretation, shown on Figure (1b), one can define new roles, as follows: (hubInW heel − , x 0 ), (hubInW heel − , y 0 ), which satisfy z 0 , x 1 ∈ (hubInW heel − , x 0 ) I , z 0 , y 1 ∈ (hubInW heel − , y 0 ) I , but z 0 , x 1 / ∈ (hubInW heel − , y 0 ) I . Now, one can define new tableau concept (constructor) denoted 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 C 0 which have to hold in some node, i.e. if

Z = {D| ∃ ∀ (hubInW heel − , x 0 ).D ∈ L(z 0 )} = {D|∀wheelInCar.D ∈ L(x 0 )} = ∅ then there exists x 1 such that z 0 , x 1 ∈ E((hubInW heel − , x 0 )) and Z ⊆ L(x 1 ).

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], B R as NFA that corresponds to role R. We use a special automaton for word w, denoted with B w . 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(C 0 ) is the smallest set of concepts in negation normal form (NNF) which contains C 0 , that is closed under ¬ and sub-concepts [6]. For a set S the f clos(C 0 , R) and ef c(C 0 , R, S) can be defined as follows:

f clos(C 0 , R) = clos(C 0 ) ∪ {∀B q R .D|∀R.D ∈ clos(C 0 ) and q is a state in B R }, ef c(C 0 , R, S) = f clos(C 0 , R) ∪ {∀B q w . ∃ ∀ (P − , s).D|s ∈ S, ∀Q.D ∈ clos(C 0 )} ∪ { ∃ ∀ (P − , s).D|s ∈ S, ∀Q.D ∈ clos(C 0 )}. Let's denote P L(B w ) = w , q |q is a state in B w , (∀w ∈ L(B q w )) w w ∈ L(B w ) . Definition 3. T=(S, L, E) is tableau for concept C 0 w.r.t. R iff 5 -S is non-empty set, -L : S → 2 ef c(C0,R,S) , -E : R C0 ∪ {(P − , s)|s ∈ S} → 2 S×S -C 0 ∈ L(s) for some s ∈ S Next, s, t ∈ S; C, C 1 , C 2 ∈ f clos(C 0 ,R); R, S ∈ R C0

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 ∀B w . ∃ ∀ (P − , s).C ∈ L(s). -(P15a) ∀Q. ∈ L(s) for all s ∈ S. -(P15b) If ∃ ∀ (P − , s).C 1 ∈ L(v)

, then there exists t with v, t ∈ E(P − , s) and

C 1 ∈ L(t). Also, for all C 2 ∈ f clos(C 0 ), if ∃ ∀ (P − , s).C 2 ∈ L(v) then C 2 ∈ L(t). -(P15c) If v, t ∈ E(P − , s), then v, t ∈ E(P − ).

Theorem 1. Concept C 0 is satisfiable w.r.t. R iff there exists tableau for C 0 w.r.t. R.

Proof. For the if direction let T = (S, L, E) be a tableau for C 0 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(C 0 ), and for roles names R = Q and Q, we set

R I = { s 0 , s n ∈ ∆ I × ∆ I | there are s 1 , . . . , s n−1 with s i , s i+1 ∈ E(S i+1 ) for 0 ≤ i ≤ n − 1 and S 1 • • • S n ∈ L(B R )}, Q I = { s 0 , s n | there are s 1 , . . . , s n−1 with s i , s i+1 ∈ E(S i+1 ) for 0 ≤ i ≤ n − 1 and S 1 • • • S n ∈ L(B Q )} ∪ { x, y |(∃z)( x, z ∈ w I and z, y ∈ E((P − , x)))}.

Let's prove that I is model for C 0 and R. I is model for R. Let's consider RIA of the form w ˙ Q • P . If x, y ∈ w I . According to (P15a) and (P6b) then ∀B w . ∃ ∀ (P − , x). ∈ L(x) holds. According to (P4a), (P15b), (P15c) and definition of Q I , P I we have (∃t) y, t ∈ E((P − , x)), y, t ∈ E(P − ) and x, t ∈ Q I , and finally implies x, y ∈ (Q • P ) I . I is model for C 0 . It is enough to prove that C ∈ L(s) implies s ∈ C I for all s ∈ S and C ∈ clos(C 0 ). 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)

∈ Q I . If ∃S 1 • • • S n−1 ∈ L(B Q ), so s i , s i+1 ∈ E(S i+1

), i = 0, . . . , n−1, s 0 = s, s n = t, then the proof is the same as proof in [6]. In case of (∃z) s, z ∈ w I and z, t ∈ 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 ∈ D I , so we have s ∈ (∀Q.D) I . For the converse, suppose that I = (∆ I , • I ) is model for C 0 w.r.t. R. Let's define tableau T = (S, L, E), as follows:

S = ∆ I , E(R) = R I , E((P − , x)) = { y, z ∈ S 2 | x, y ∈ w I , x, z ∈ Q I , z, y ∈ P I }, and L(s) = {C ∈ clos(C 0 )|s ∈ C I }∪{∀B R .C|∀R.C ∈ clos(C 0 ) and s ∈ (∀R.C) I }∪ {∀B q R .C ∈ f clos(C 0 , R)| for all S 1 • • • S n ∈ L(B q R ), s ∈ (∀S 1 . ∀S 2 • • • ∀S n .C) I , and if ε ∈ L(B q R ) then s ∈ C I } ∪ {∀Q. } ∪ {∀B w . ∃ ∀ (P − , s).C|s ∈ (∀Q.C) I } ∪ {∀B q w . ∃ ∀ (P − , t

).C|(∃w ) w , q ∈ P L(B w ) and t, s ∈ (w ) I and t ∈ (∀Q.C) I } ∪ { ∃ ∀ (P − , t).C| t, s ∈ w I and t ∈ (∀Q.C) I }. Let's prove that T is tableau for C 0 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).C 1 ∈ L(v). From the definition of L(v) follows s, v ∈ w I and s ∈ (∀Q.C) I . Because of I |= w ˙ Q • P we have that there exists z such that s, z ∈ Q I and z, v ∈ P I i.e. v, z ∈ E((P − , s)). On the other hand, from s ∈ (∀Q.C) I and s, z

∈ Q I follows z ∈ C I 1 , so C 1 ∈ L(z). If ∃ ∀ (P − , s).C 2 ∈ L(v) then s ∈ (∀Q.C 2 ) I , so z ∈ C I 2 , i.e. C 2 ∈ L(z).

Tableau algorithm

The tableau algorithm generates completion tree.

Definition 4. (Completion tree) Completion tree for

C 0 w.r.t R is labelled tree G = (V, E, L, ˙ =) where each node x ∈ V is labelled with a set L(x) ⊆ ef c(C 0 , R, V ) ∪ {≤ mR.C| ≤ nR.C ∈ clos(C 0 ), m ≤ n}. Each edge x, y ∈ E is labelled with a set L x, y ⊆ R C0 ∪ {(P − , s)|s ∈ V }.

Additionally, we care of inequalities between nodes in V , of the tree G, with a symmetric binary relation ˙ =.

If x, y ∈ 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 R with R * R, R ∈ L( x, y ). 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 ∈ R C0 , x ∈ V , C ∈ clos(C 0 ) we define set S G (x, C) = {y|y is S − neighbour of x and C ∈ L(y)} 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 {y 0 , . . . , y n } ∈ S G (x, C) with y i ˙ =y j for all 0 ≤ i < j ≤ n.

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(C 0 , 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 w ˙ Q • P . Let's suppose that language L(B w ) is finite.

If ∀B q w . ∃ ∀ (P − , s).C ∈ L(t) then there exists (w , q) ∈ P L(B w ) and (s, t) ∈ E(w ). If n = f clos(C 0 , R), l = max{len(w )|(∃q)(w , q) ∈ P L(B w )} and number of successors is less than m (different than P − neighbours), then 6 : L(t) ≤ n• m l • P L(B w ). To illustrate the technique in an understandable way, we consider only special case, when L(B w ) = {R}. Definition 6. Let G = (V, E, L, ˙ =) be completion tree and f :

V → V is a function. -f (x) = y, -L(x) ∩ f clos(C 0 , R) = L(y) ∩ f clos(C 0 , R), -R ∈ L( z, x ) ⇔ R ∈ L( f (z), y ), -∃ ∀ (P − , z).C ∈ L(x) ⇔ ∃ ∀ (P − , f (z)).C ∈ L(y). 2. We say that L( x, y ) f − match with L( u, v ), denoted with L( x, y ) ∼ f L( u, v ), if -L( x, y ) ∩ R C0 = L( u, v ) ∩ R C0 , -(∀s ∈ V )((P − , s) ∈ L( x, y ) ⇔ (P − , f (s)) ∈ L( u, v )).

Definition 7. (Blocking) A node x is label blocked if there is a function f : V → V and there are predecessors x , y, y of the node x, such that

-x = y, -x is successor of x and y is successor of y , -L(x) ∼ f L(y), L(x ) ∼ f L(y ), -L( x, x ) ∼ f L( y, y ).

In this case we say that y blocks x.

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 x and y and (finite number of) R-neighbours of these four nodes. For the nodes, function f can be nondeterministically 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 C 0 and RBox R, -Output: "Yes" if concept C 0 is satisfiable w.r.t. RBox R, otherwise "No" -Method: 1. step: Construct tree G = (V, E, L, ˙ =), where V = {x 0 }, E = ∅, L(x 0 ) = {C 0 }. 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 C 0 and R, 2. Tableau algorithm returns answer "Yes" iff there exists tableau of the concept C 0 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 (x , 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.

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 R ˙ Q•P , we can apply the technique to RIA of the form

S 1 S 2 • • • S n ˙ R 1 R 2 • • • R m ,

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 w ˙ QP when the language L(B w ) is infinite.