A Decidable Extension of SRIQ with Disjunctions in Complex Role Inclusion Axioms Milenko Mosurović1 , Henson Graves2 , and Nenad Krdžavac3 1 Faculty of Mathematics and Natural Science, University of Montenegro, Podgorica, ul. Džordža Vašingtona bb, 81000 Podgorica, Montenegro. milenko@ac.me 2 Algos Associates, 2829 West Cantey Street, Fort Worth, TX 76109 United States henson.graves@hotmail.com 3 Department of Accounting and Information Systems, College of Business and Law, University College Cork, Cork City, Ireland. N.Krdzavac@ucc.ie Abstract. This paper establishes the decidability of SR⊔ IQ which has composition-based role Inclusion axioms (RIAs) of the form R1 ◦ · · · ◦ ˙ 1 ⊔ · · · ⊔ Tm . Also the consistency of an Abox A of SR⊔ IQ DL Rn ⊑T w.r.t. Rbox R is established. Motivation for this kind of RIAs comes from applications in the field of manufactured products as well as other con- ceptual modeling applications such as family relationships. The solution is based on a tableau algorithm. Keywords: Description Logic, Manufacturing system,Tableau, Composition- based Role Inclusion Axiom. 1 Introduction Description logic (DL) [1] has focused on extending decidability results to DLs with more complex RIAs [6, 7, 9]. However, the logic SROIQ DL which is logi- cal basis for the standard Ontology Web Language OWL 2 [3], does not admit assertions which have role unions on the right hand side of RIAs. Many applica- tions involve RIAs with role unions on the right side. For example in modeling an engine in a car that can power wheelInCar or oilPump or generator, or all of these, at the same time [8, 2]. This model can be described in the following composition-based RIAs [11]: engineInCar ◦ powers ⊑ wheelInCar ⊔ generatorInCar ⊔ oilP unInCar (1) One can conclude that for an individual car c1 and an individual p1 : if p1 is powered by an individual engine e1 in the car c1 then p1 is an individual wheel or a generator or an oilpump in c1 . The RIA of the form (1) ca be expressed in an extension of ALC DL with composition-based RIAs [11], but SROIQ DL does not support such composition-based RIAs. Modeling such RIAs in the extensions of ACL DL considered only two roles on the left hand side of the RIAs. This paper introduces the SR⊔ IQ DL that extends SRIQ DL [5] with composition-based RIAs of the form (2). As noted in [11] the RIA of the form (2) are not role value-maps [10]. The logic analyzed in this paper overcomes the following shortcomings of the logics studied in [11]: 1. Finite automata handle composition-based RIAs of the form (2). 2. Does not require a Rbox to be admissible [11], 3. Does not require all roles to be disjoint [11], 4. Allows more than two roles on the left hand side of composition-based RIAs. The rest of the paper is organized as follows. Next section gives definition of SR⊔ IQ DL. Section 3 defines tableau for SR⊔ IQ and proves decidability of the logic. The section also gives and example of tableau for RIA of the form (2). The last section concludes the paper. 2 Preliminaries The alphabet of SRIQ and SR⊔ IQ DL consists of set of concept names NC , set of role names NR , set of simple role names NS ⊂ NR and finally, a set of individual names NI . The set of roles is NR ∪ {R− |R ∈ NR } and on this set the function Inv(·) is defined as Inv(R) = R− and Inv(R− ) = R for R ∈ NR . A role chain is a sequence of roles w = R1 R2 . . . Rn . SR⊔ IQ language is an extension of SRIQ [5], by allowing new kinds of RIAs in role hierarchy. The syntax of the SR⊔ IQ DL concepts, Rbox, Tbox and Abox are given in definitions 1, 2 and 3 following [5]. Definition 1. Set of SR⊔ IQ 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 ⊓D, C ⊔D, ∀R.C, ∃R.C, ∃S.Self , (≤ nS.C), (≥ nS.C) are concepts. A general concept inclusion axiom (GCI) is an expression of the form C ⊑D ˙ for ⊔ two SR IQ-concepts C and D. A Tbox T is a finite set of GCIs. An individual assertion has one of the following forms: a : C, (a, b) : R, (a, b) : ¬S, or a̸=˙ b, for a, b ∈ NI (the set of individual names), a (possibly inverse) role R, a (possibly inverse) simple role S, and a SR⊔ IQ-concept C. A SR⊔ IQ-Abox A is a finite set of individual assertions. A (composition-based) RIA is a statement of the form [11]: R1 · · · Rn ⊑T ˙ 1 ⊔ · · · ⊔ Tm . (2) Without additional restrictions on RIAs, some DLs [11] with composition- based RIAs are undecidable. Definition 2. Strict partial order ≺ (irreflexive, transitive, and antisymmetric), on the set of roles, provides acyclicity [5]. Allowed RIAs in SRIQ DL with respect to ≺, are expressions of the form w⊑R, ˙ where [4, 5]: 1. R is a simple role name, w = S is a simple role, and S ≺ R or S = R− or 2. R ∈ NR \NS is a role name and w = RR, or w = R− , or w = S1 · · · Sn and Si ≺ R, for 1 ≤ i ≤ n, or w = RS1 · · · Sn and Si ≺ R, for 1 ≤ i ≤ n, or w = S1 · · · Sn R and Si ≺ R, for 1 ≤ i ≤ n A SRIQ role hierarchy is a finite set R1h of RIAs. A SRIQ role hierarchy R1h is regular if there exists strict partial order ≺ such that each RIA in R1h is allowed with respect to ≺ [4, 5]. Definition 3. A SR⊔ IQ role hierarchy is a finite set Rh = R1h ∪ R2h , where R1h is SRIQ role hierarchy and Rh2 is set of RIA Ri1 · · · Rini ⊑ Ti1 ⊔ · · · ⊔ Timi , and Tij are not simple roles, for i = 1, . . . , k. A SR⊔ IQ role hierarchy Rh is regular if R1h is regular and Tij does not appear on the left hand side of RIAs in Rh . A SR⊔ IQ set of role assertions is a finite set Ra of the assertions Ref (R), Irr(S), Sym(R), Tra(V), and Dis(T, S), where R is a role, S, T are simple roles and V is not simple role [5]. A SR⊔ IQ Rbox R = Rh ∪ Ra , where Rh is SR⊔ IQ role hierarchy and Ra is a set of role assertions. If R1h is regular w.r.t strict partial order ≺ then we extend ≺ such that Rij ≺ Til hold, i = 1, . . . , k and j = 1, . . . , ni , l = 1, . . . , mi . Further, we assume that labels, such as k, ni , mi , Til , Rij , have the same meaning as defined in definition 3. Definition 4. The semantics of the SR⊔ IQ DL is defined by using interpre- tation. 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 con- cept name C with a subset C I ⊆ ∆I ; every role name R with a binary relation RI ⊆ ∆I × ∆I and, every individual name a with an element aI ∈ ∆I [1]. Definition 5. An interpretation I extends to SR⊔ IQ complex concepts and roles according to the following semantic rules: – If R is a role name, then (R− )I = {⟨x, y⟩ : ⟨y, x⟩ ∈ RI }, – If R1 , R2 ,. . . , Rn are roles then (R1 R2 . . . Rn )I = (R1 )I ◦ (R2 )I ◦ · · · ◦ (Rn )I and (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 4 ⊤I = ∆I , ⊥I = ∅, (¬C)I = ∆I \C I , (C ⊓ D)I = C I ∩ DI , (C ⊔ D)I = C I ∪ DI , (∃R.C)I = {x : ∃y. ⟨x, y⟩ ∈ RI ∧ y ∈ C I }, 4 ♯M denotes cardinality of set M . (∃S.Self )I = {x : ⟨x, x⟩ ∈ S I }, (∀R.C)I = {x : ∀y. ⟨x, y⟩ ∈ RI ⇒ y ∈ C I }, (≥ nS.C)I = {x : ♯{y : ⟨x, y⟩ ∈ S I , y ∈ C I } ≥ n}, (≤ nS.C)I = {x : ♯{y : ⟨x, y⟩ ∈ S I , y ∈ C I } ≤ n}. Inference problems for SR⊔ IQ are defined in standard way [5]. Definition 6. An interpretation I satisfies a RIA R1 · · · Rn ⊑T ˙ 1 ⊔ · · · ⊔ Tm , if I I I I R1 ◦ · · · ◦ Rn ⊆ T1 ∪ · · · ∪ Tm . An interpretation I is model of a – Tbox T (written I |= T ) if C I ⊆ DI for each GCI C ⊑D ˙ in T . – role hierarchy Rh , if it satisfies all RIAs in Rh (written I |= Rh ). – role assertions Ra (written as I |= Ra ) if I |= Φ holds for each role assertion axiom Φ ∈ Ra , where is I |= Dis(S, R) if S I ∩ RI = ∅, I |= Sym(R) if RI is symmetric relation , I |= T ra(R) if RI is transitive relation , I |= Ref (R) if RI is reflexive relation, I |= Irr(S) if RI is irreflexive relation. – Rbox R = ⟨Rh , Ra ⟩ (written as I |= R) if I |= Rh and I |= Ra . – Abox A (I |= A) if for all individual assertions ϕ ∈ A we have I |= ϕ, where I |= a : C if aI ∈⟨C I , ⟩ I |= a̸= ˙ b if aI ̸= bI , ⟨ ⟩ I |= (a, b) : R if a , b ∈ R , I |= (a, b) : ¬R if aI , bI ∈ I I I / RI . For an interpretation I, an element x ∈ ∆I is called an instance of a concept C if x ∈ C I . An Abox A is consistent with respect to a Rbox R and a Tbox T if there is a model I for R and T such that I |= A. Definition 7. A concept C is called satisfiable if there is an interpretation I with C I ̸= ∅. A concept D subsumes a concept C (written C ⊑D) ˙ if C I ⊆ DI holds for each interpretation. Two concepts are equivalent (written C ≡ D) if they are mutually subsuming. All standard inference problems for SR⊔ IQ-concepts and Abox can be re- duced [5] to the problem of determining the consistency of a SR⊔ IQ-Abox w.r.t. a Rbox, where we can assume w.l.o.g. that all role assertions in the Rbox are of the form Dis(S, R). We call such Rbox reduced. 3 The Extension of SRIQ Tableau Let A be a SR⊔ IQ-Abox and R a reduced SR⊔ IQ-Rbox and let RA be a set of role names appearing in A and R, including their inverse, and IA is the set of individual names appearing in A. To check whether Abox A is consistent w.r.t. Rbox R we transform SR⊔ IQ-Rbox R to SRIQ-Rbox R′ as follows: 1. For each role name R ∈ RA we define equivalence class [R] = {R} and set [R− ] = [R]− , comp([R]) = {R}, comp([R− ]) = {R− }, 2. For each RIA of the form Ri1 · · · Rini ⊑ Ti1 ⊔ · · · ⊔ Timi ∈ R (1 ≤ i ≤ k) we define equivalence class [Ti1 ⊔· · ·⊔Timi ] = {Tj1 ⊔· · ·⊔Tjmj | {Ti1 , . . . , Timi } = {Tj1 , . . . , Tjmj }, 1 ≤ j ≤ k} and set comp([Ti1 ⊔· · ·⊔Timi ]) = {Ti1 , . . . , Timi } {∀hGm.W, ∀hGm.G, ∀hGf.M, ∀hGf.B} ⊆ L(M ary) {∀hP.∀hP.(Z1 ∨ Z2 )} M ary hP hGm Z1 = (hGm, {W, G}, ∅) P arent1 Z2 = (hGf, {M, B}, ∅) hP Z 1 ∨ Z2 x {W, G} ⊆{ W, G, B, ¬M } Fig. 1. A part of tableau for (3) and (4) 3. We consider equivalence classes [R], previously defined, as role names which do not appear in RA . Set of the role names is denoted with R′A . Let’s define R′ = {[R1 ] · · · [Rn ]⊑[T ˙ 1 ⊔ · · · ⊔ Tm ] | R1 · · · Rn ⊑T ˙ 1 ⊔ · · · ⊔ Tm ∈ R}. If Rbox R is regular w.r.t order ≺ then Rbox R′ is regular w.r.t ≺′ defined as follows [R] ≺′ [S] iff R ≺ S and [Tij ] ≺′ [Ti1 ⊔ · · · ⊔ Timi ], j = 1, ..., mi , i = 1, ..., k. Equivalence classes and order ≺′ previously defined are using for automata construction. For the following example of RIAs R1 R2 ⊑ H1 ⊔ H2− and S1 S2 ⊑ H2− ⊔ H1 one should construct a nondeterministic finite automaton (NFA) for role [H1 ⊔ H2− ]. The automaton should accept words R1 R2 and S1 S2 . Namely, for every role [R] we have kept the construction of NFA B[R] based on R′ , as same as defined in [5]. 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). To illustrate main idea in this paper, we use the following simple example. Example 1. In this example we use the following abbreviations: hP = hasP are- nt, hGm = hasGrandM other, hGf = hasGrandF ather, W = W oman, M = M an, G = Gentle, B = Blabber. We defined the following RIA: hP ◦ hP ⊑ hGm ⊔ hGf (3) and the individual assertion: M ary : ∀hGm.W ⊓ ∀hGf.M ⊓ ∀hGm.G ⊓ ∀hGf.B (4) We should decide whether x (see Fig. 1) is instance of GrandM other or GrandF ather. If x ∈ GrandM otherI then x ∈ W I , x ∈ GI . In the case of (M ary, x) ∈ hGmI , it does not break syntax rules. Similar to this one, if x ∈ GrandF atherI then x ∈ M I , x ∈ B I and (M ary, x) ∈ hGf I hold. Meta- labels Z1 and Z2 are using to remember the (relevant) parts of the labels in the node M ary which should be transferred from the node to node x (see Fig. 1). First component in Z1 is role. The second component is the set of the concepts {C|M ary is instance of concept ∀hGm.C}. The third component is the set of concepts, for which M ary is instance and should be superset of the set {C|x is instance of concept ∀hGm− .C}. Because of inverse role we need first and third component. To choose given meta-label, we note as Z1 ∨ Z2 . To recognize path hP ◦ hP from node M ary to x we use NFA B[hGm⊔hGf ] noted as follows ∀B[hGm⊔hGf ] .(Z1 ∨ Z2 ).  We assume that all concepts are in negation normal form (NNF). For given concept C0 , clos(C0 ) is the smallest set that contains C0 and that is closed under sub-concepts and ¬.˙ We use ¬C ˙ for NNF of ¬C [5]. We use two sets of the label of nodes. First set is [5]: clos(A) := ∪a:C∈A clos(C). The second set is: N F Aclos(A, R) := {∀B[R] q .Z| [R] ∈ R′A and q is state in NFA B[R] and ∨ Z = T ∈comp([R]) (T, ZT , ẐT ), ZT ⊆ clos(A)|T , ẐT ⊆ clos(A)|T − }, where clos(A)|Q = {C | ∀Q.C ∈ clos(A)}. { In the proofs of decidability ( set P L(B[R] ) = ⟨w′ , q⟩ |q is a state in we use )} B[R] , (∀w′′ ∈ L(B[R] q )) w′ w′′ ∈ L(B[R] ) . Set P L(B[R] ) contains pairs of the form (w , q). First component w′ is prefix of a word w ∈ L(B[R] ), but the second ′ component q is a state of automaton B[R] which can be reached if input word for the automaton has prefix w′ . Definition 8. T = (S, L, L, E, J ) is a tableau for A with respect to R iff a) S is non-empty set, b) L : S → 2clos(A) , c) L : S → 2N F Aclos(A,R) , d) J : IA → S, e) E : RA → 2S×S . Furthermore, for all C, C1 , C2 ∈ clos(A); s, t ∈S; R, S ∈ RA , and a, b ∈ IA , the tableau T satisfies: – (P1a) If C ∈ L(s), then ¬ C ∈ / L(s) (C is atomic, or ∃R.Self ), – (P1b) ⊤ ∈ L(s), and ⊥ ∈ / L(s), for all s, – (P1c) If ∃R.Self ∈ L(s), then ⟨s, s⟩ ∈ E(R), – (P2) if (C1 ⊓ C2 ) ∈ L(s), then C1 ∈ L(s) and C2 ∈ L(s), – (P3) if (C1 ⊔ C2 ) ∈ L(s), then C1 ∈ L(s) or C2 ∈ L(s), – (P5) if ∃S.C ∈ L(s), then there is some t with ⟨s, t⟩ ∈ E(S) and C ∈ L(t), – (P7) ⟨x, y⟩ ∈ E(R) iff ⟨y, x⟩ ∈ E(Inv(R)), – (P8) if (≤ nS.C) ∈ L(s), then ♯S T (s, C) ≤ n, – (P9) if (≥ nS.C) ∈ L(s), then ♯S T (s, C) ≥ n, – (P10) if (≤ nS.C) ∈ L(s) and ⟨s, t⟩ ∈ E(S), then C∈ L(t) or ¬C ˙ ∈ L(t), – (P11) if a : C ∈ A, then C ∈ L(J (a)) – (P12) if (a, b) : R ∈ A, then (J (a), J (b)) ∈ E(R), – (P13) if (a, b) : ¬R ∈ A, then (J (a), J (b)) ∈ / E(R), ˙ b ∈ A, then J (a) ̸= J (b), – (P14) if a̸= – (P15) if Dis(R, S) ∈ R, then E(R) ∩ E(S) = ∅, – (P16) if ⟨s, t⟩ ∈ E(R) and R ⊑∗ S, then ⟨s, t⟩ ∈ E(S),5 ⊑ 5 ∗ is the transitive closure of ⊑ [5] ∨ – (P6’) ∀B[R] .Z ∈ L(s), where 6 Z = Q∈comp([R]) (Q, ZQ , ẐQ ), ZQ = L(s)|Q = {C|∀Q.C ∈ L(s)} and ẐQ = L(s) ∩ clos(A)|Q− , for all s ∈ S and [R] ∈ R′A , S – (P4a’) if ∀B .Z ∈ L(s), ⟨s, t⟩ ∈ E(S), and p → q ∈ B , then ∀B .Z ∈ L(t), p p q ∨l – (P4b’) if ∀Bp .Z ∈ L(s), ε ∈ L(B p ), and Z = j=1 (Qj , Zj , Ẑj ) then there is j0 , such that Zj0 ⊆ L(s), L(s)|Q− ⊆ Ẑj0 j0 where in (P8) and (P9), ′ ′ S T (s, C) = {t ∈ S| ⟨s, t⟩ ∈ E(S ), for some S ∈ L(BS ) and C ∈ L(t)}. Lemma 1. SR⊔ IQ-Abox A is consistent w.r.t. R iff there exists a tableau for A w.r.t. R. Proof. (⇐)Let T = (S, L, L, E, J ) be a tableau for A with respect to R. An interpretation I = (∆I , ·I ) of A and R can be defined as follows: ∆I := S, C I := {s|C ∈ L(s)}, for a concept name C ∈ clos(A), aI := J (a) for an individual name a ∈ IA and for a role name [Q] ∈ R′A , R ∈ RA , we set E([Q]) := {⟨s0 , sn ⟩ ∈ ∆I ×∆I | there are s1 , · · · , sn−1 with ⟨si , si+1 ⟩ ∈ E(Si+1 ), for 0 ≤ i ≤ n − 1 and S1 S2 · · · Sn ∈ L(B[Q] )}, RI := {⟨x, y⟩ ∈ ∪R∈comp([Q]) E([Q])|L(x)|R ⊆ L(y) and L(y)|R− ⊆ L(x)}. We have to show that I is a model for A and R. Next, we show that I is model for R. I |= Ra can be proved by using the same method as in [5]. Let’s consider a RIA of the form R1 · · · Rn ⊑T ˙ 1 ⊔ · · · ⊔ Tm . Let’s ⟨x0 , xn ⟩ ∈ (R1 · · · Rn )I . According to semantic rules, there are x1 , ..., xn−1 such I that ⟨xi , xi+1 ⟩ ∈ Ri+1 , for i = 0, 1, ..., n−1. As roles Tij do not appear on the left hand side of RIAs then Ri ∈ comp([Q]) only for Q = Ri i.e. RiI ⊆ E([Ri ]). This means that there are yi0 = xi , yi1 ,...,yili = xi+1 such that ⟨yij , yij+1 ⟩ ∈ E(Sij+1 ) and Si1 · · · Sili ∈ L(B[Ri+1 ] ). According to automata construction, we have the following: S11 · · · S1l1 S21 · · · Snln ∈ L(B[T1 ⊔···⊔Tm ] ) so ⟨x0 , xn ⟩ ∈ E([T1 ⊔· · ·⊔Tm ]). On the other side, according to rule (P6’), the following ∀B[T1 ⊔···⊔Tm ] .Z ∈ L(x0 ) ∨m holds, where Z = j=1 (Tj , ZTj , ẐTj ). By S11 · · · Snln ∈ L(B[T1 ⊔···⊔Tm ] ) and rule q q (P4a’) we have ∀B[T 1 ⊔···⊔Tm ] .Z ∈ L(xn ) and ε ∈ L(B[T 1 ⊔···⊔Tm ] ). From (P4b’) we have that there is j such that L(x0 )|Tj = ZTj ⊆ L(xn ) and L(xn )|T − ⊆ ẐTj ⊆ j L(x0 ), i.e. ⟨x0 , xn ⟩ ∈ TjI . Therefore ⟨x0 , xn ⟩ ∈ (T1 ⊔ · · · ⊔ Tm )I . Secondly, we prove that I is model for A. We show that C ∈ L(s) implies s ∈ C I for each s ∈ S and each C ∈ clos(A). Together with (P11)-(P14), this implies that I is a model for A [5]. Consider the case C ≡ ∀R.D. For the other cases, see [5]. Let ∀R.D ∈ L(s) and ⟨s, t⟩ ∈ RI . If R is role name then according to definition RI there exists [Q] such that R ∈ comp([Q]), ⟨s, t⟩ ∈ E([Q]) and L(s)|R ⊆ L(t). If R = S − , where S role name, then according to definition S I there exists role [Q] such that S ∈ comp([Q]), ⟨t, s⟩ ∈ E([Q]) and L(s)|S − ⊆ L(t) (i.e. L(s)|R ⊆ L(t)). In both cases we have D ∈ L(t). By induction, t ∈ DI and thus s ∈ (∀R.D)I . 6 Rules (P6), (P4a) and (P4b) in [5] are changed with rules (P6’), (P4a’) and (P4b’). (⇒) For the converse, suppose I = (∆I , ·I ) is a model for A w.r.t. R. We define tableau T = (S, L, L, E, J ) as follows: S := ∆I , J (a) := aI , E(R) := RI , L(s) := {C ∈ clos(A)}|s ∈ C I } L(s) := {∀B[R]q .Z|(∃t ∈ ∆I )(∃w′ )∀B[R] .Z ∈ L1 (t), ⟨w′ , q⟩ ∈ P L(B[R] ) and ⟨t, s⟩ ∈ ∨ (w′ )I }, where L1 (s) := {∀B[R] .Z|Z = Q∈comp([R]) (Q, L(s)|Q , L(s)∩clos(A)|Q− )}. We have to prove that T is tableau for A w.r.t R. We restrict our attention to the only new cases. For the other cases, see [5]. The rule (P6’) follows immediately from the definition of L1 (s) and L1 (s) ⊆ L(s) (for t = s and w′ = ε). For (P 4a′ ), let’s ∀B[R] p .Z ∈ L(s), ⟨s, t⟩ ∈ E(S). Assume that there is a transition S p → q ∈ B[R] p . From definition L(s) there exists v ∈ ∆I and w′ such that ∀B[R] .Z ∈ L1 (v), ⟨w′ , p⟩ ∈ P L(B[R] ) and ⟨v, s⟩ ∈ (w′ )I . Let’s w′′ = w′ S then ⟨w′′ , q⟩ ∈ P L(B[R] ) and ⟨v, t⟩ ∈ (w′′ )I , so ∀B[R] q .Z ∈ L(t). p p ∨l For (P4b’), let’s ∀B[R] .Z ∈ L(s), ε ∈ L(B[R] ), and Z = j=1 (Qj , Zj , Ẑj ). By definition L(s) there exists x ∈ ∆I and w′ such that ∀B[R] .Z ∈ L1 (x), ⟨w′ , q⟩ ∈ P L(B[R] ) and ⟨x, s⟩ ∈ (w′ )I . Further, we have [R] = [Q1 ⊔ · · · ⊔ Ql ], Zj = L(x)|Qj and Ẑj = L(x) ∩ clos(A)|Q− . By ε ∈ B[R] p we have w′ ∈ L(B[R] ), so j I w′ ⊆ (Q1 ⊔ · · · ⊔ Ql )I , i.e. ⟨x, s⟩ ∈ (Q1 ⊔ · · · ⊔ Ql )I . This means that there is j such that ⟨x, s⟩ ∈ QIj . By the rules of semantics and the definition of L(s), we have Zj = L(x)|Qj ⊆ L(s) and L(s)|Q− ⊆ L(x) ∩ clos(A)|Q− = Ẑj . j j ⊔ Tableau algorithm for SR IQ DL works on the completion forest on similar manner as described in [5]. Definition 9. (Completion forest) Completion forest for a SR⊔ IQ-Abox A and a Rbox R is a labeled collection of trees G = (V, E, L, L, ̸=˙ ) whose distinguished root nodes can be connected arbitrarily, where each node x ∈ V is labeled with two sets L(x) ⊆ clos(A) and L(x) ⊆ N F Aclos(A, R). Each edge ⟨x, y⟩ ∈ E is labeled with a set L(⟨x, y⟩) ⊆ RA . Additionally, we care of inequalities between nodes in V , of the forest 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 neighbor (R-neighbor) 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 ∈ RA , x ∈ V , C ∈ clos(A) we define set S G (x, C) = {y|y is S − neighbour of x and C ∈ L(y)} Definition 10. A completion forest 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 – x is an S-neighbor of x and ¬∃S.Self ∈ L(x), or – x and y are root nodes, y is an R-neighbor of x, and ¬R ∈ L(⟨x, y⟩), or – there is some Dis(R, S) ∈ Ra and y is an R and an S-neighbor of 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 ̸= ∨l – there is ∀Bp .Z ∈ L(x), with ε ∈ L(Bp ), Z = j=1 (Qj , Zj , Ẑj ) and there are no j such that L(x)|Q− ⊆ Ẑj . j A completion forest that does not contain a clash is called clash-free. ⊓ ⊔ The blocking is employed in order to have termination [5]. Definition 11. A node is called blocked if it is either directly or indirectly blocked [5]. A node x is directly blocked if none of its ancestors are blocked, and it has ancestors x′ , y and y ′ such that [5]: – none of x′ , y and y ′ is a root node, – x is a successor of x′ and y is a successor of y ′ , and – L(x) = L(y) and L(x′ ) = L(y ′ ), and – L(x) = L(y) and L(x′ ) = L(y ′ ), and – L(⟨x′ , x⟩) = L(⟨y ′ , y⟩). In this case we say that y blocks x. A node y is indirectly blocked if one of its ancestors is blocked [5]. The non-deterministic tableau algorithm can be described as follows: – Input: Non-empty SR⊔ IQ-Abox A and a reduced Rbox R – Output: ”Yes” if SR⊔ IQ-Abox A is consistent w.r.t. Rbox R, otherwise ”No” – Method: 1. step: Construct completion forest G = (V, E, L, L, ̸= ˙ ) as follows: • for each individual a occurring in A, V contains a root node xa , • if (a, b) : R ∈ A or (a, b) : ¬R ∈ A, then E contains an edge ⟨xa , xb ⟩, • if a̸=˙ b ∈ A, then xa ̸= ˙ xb is in G, • L(xa ) := {C|a : C ∈ A}, • L(xa ) := ∅, • L(⟨xa , xb ⟩) := {R|(a, b) : R ∈ A} ∪ {¬R|(a, b) : ¬R ∈ A} Go to step 2. 2. step: Apply an expansion rule (see table 1) to the forest G, while it is possible. Otherwise, go to step 3. 3. step: If the forest G does not contain clash return ”Yes”, otherwise return ”No”. Lemma 2. Let A be a SR⊔ IQ-Abox and R a reduced Rbox. The tableau algo- rithm terminates when started for A and R. Lemma 3. Let A be a SR⊔ IQ-Abox and R a reduced Rbox. Tableau algorithm returns answer ”Yes” if and only if there is a tableau for A w.r.t. R. Table 1. Expansion rules for SR⊔ IQ tableau algorithm (updated from [5]) The rules ⊓, ⊔, ∃, Self, ≤r , ≥, ≤ are defined in [5], but only in rules that create new node y should set L(y) := ∅ ch′ If x is not indirectly blocked and there is concept C ∈ clos(A) with {C, ¬C}˙ ∩ L(x) = ∅ then L(x) → L(x) ∪ {E}, for some E ∈ {C, ¬C} ˙ ∀′1 If x is not indirectly blocked and it is not possible to apply ch′ -rule to L(x), ∨ and ∀B[R] .Z ∈/ L(x), where Z = Q∈comp([R]) (Q, L(x)|Q , L(x) ∩ clos(A)|Q− ) then L(x) → L(x) ∪{∀B[R] .Z} ∀′2 If ∀Bp .Z ∈ L(x), and x is not indirectly blocked, p → q ∈ Bp and S there is S-neighbor y of x with ∀Bq .Z ∈ / L(y) then L(y) → L(y)∪ {∀Bq .Z} ∀′3 If ∀Bp .Z ∈ L(y), and y is not indirectly blocked, ε ∈ L(Bp ), ∨ Z = lj=1 (Qj , Zj , Ẑj ) and there is no j such that Zj ⊆ L(y) and L(y)|Q− ⊆ Ẑj j then choose j such that L(y)|Q− ⊆ Ẑj and L(y) → L(y) ∪ Zj . j Proof. For the if direction, suppose that the algorithm returns ”Yes”. It means ˙ ) without clash that the algorithm generated completion forest G = (V, E, L, L, ̸= and there are no expansion rules (see table 1) that can be applied. Let’s b(x) = x, if x is not blocked and b(x) = y, if y blocks node x. A path [6] is a sequence of pairs nodes of G of the form p = ⟨(x0 , x′0 ), . . . , (xn , x′n )⟩ . (5) For such a path, we define T ail(p) = xn and T ail′ (p) = x′n . We denote the path ⟨ ⟩ (x0 , x′0 ), (x1 , x′1 ), . . . , (xn , x′n ), (xn+1 , x′n+1 ) (6) ⟨ ⟩ with p|(xn+1 , x′n+1 ) . The set of P aths(G) can be defined inductively as follows: – if x0 is root node then ⟨x0 , x0 ⟩ ∈ P aths(G) – if p ∈ P aths(G), z ∈ V and z is not indirectly blocked, such that ⟨T ail(p), z⟩ ∈ E, then (p, ⟨b(z), z⟩) ∈ P aths(G) We define structure T = (S, L, L, E, J ) as follows S := P aths(G), L(p) := L(T ail(p)), L(p) := L(T ail(p)), if root node xa denotes individual a then J (a) = (⟨xa , xa ⟩) and E(R) := {⟨s, t⟩ ∈ S × S|t = (s, ⟨b(y), y⟩) and y is an R − successor of T ail(s) or s = (t, ⟨b(y), y⟩) and y is an Inv(R)−successor of T ail(t)} ∪{⟨J (a), J (b)⟩ |xb is an R-neighbour of xa }. Thus defined structure T is a tableau. New rules (P6’), (P4a’) directly follows from ∀′1 and ∀′2 rule, but (P4b’) follows from ∀′3 and definition of clash (see definition (10)). For the other cases, see [6]. For the only-if direction, the proof is the same as proof in [4, 5] (i.e., we take a tableau and use it to steer the application of the non-deterministic rules). From Theorem 1 in [5] and Lemmas 1, 2 and 3, we thus have the following theorem: Theorem 1. The tableau algorithm decides satisfiability and subsumption of SR⊔ IQ-concepts with respect to Aboxes, Rboxes, and Tboxes. 4 Conclusion It is important to note that original idea of extension ALC DL with composition- based RIAs is presented in [11]. We introduce more expressive formalism that allows composition-based RIAs and relaxed restrictions defined in [11]. Moti- vated by practical applications in manufacturing engineering we define tableau algorithm in order to check satisfiability of SR⊔ IQ DL. Future research will be focused on how to extend regularity conditions for SROIQ DL in order to sup- port composition-based RIAs as well as at the same time support RIAs proposed in [9]. We use the algorithm proposed in this paper for modeling the regulations of capital adequacy of credit institutions. References 1. Baader, F. Calvanese, D., McGuinness, D., Nardi D., Patel-Schneider, P.: The description logic handbook - theory, implementation and application. Cambridge University Press, second edition (2007) 2. Bock, C., Zha, X., Suh, H., Lee, J.: Ontological product modeling for collaborative design. Advanced Engineering Informatics 24 (2010) 510-524 3. Grau, B. C., Horrocks, I., Motik, B., Parsia, B., Schneider, P. P., Sattler, U: OWL 2: The next step for OWL, Journal of Web Semantics: Science, Services and Agents on the World Wide Web 6(4) (2008) 309-322 4. Horrocks, I., Sattler, U.: Decidability of SHIQ with complex role inclusion axioms. Artificial Intelligence 160(1-2) (2004) 79-104 5. I. Horrocks, O. Kutz, and U. Sattler. The irresistible SRIQ. In Proceedings of the OWLED*05 Workshop on OWL: Experiences and Directions and Technical Report, 2005. http://www.cs.man.ac.uk/~sattler/publications/sriq-tr.pdf 6. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In Pro- ceedings of the 10th International Conference on Principles of Knowledge Repre- sentation and Reasoning (KR 2006). (2006) 57-67 7. Kazakov, Y.: 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), Edinburgh, UK. (2010) 472-487 8. Krdžavac, N., Bock, C.: Reasoning in manufacturing part-part examples with OWL2. U.S. National Institute of Standards and Technology, Technical Report NISTIR 7535. (2008) 9. Mosurović, M., Krdžavac, N.: A thechnique for handling the right hand side of com- plex RIA. In Proc. of 24th International Workshop on Description Logics (DL2011), Barselona, Spain. (2011) 543-554 10. Schmidt-Schaus, M.: Subsumption in KL-ONE is undecidable. In Principle of Knowledge Representation and Reasoning-Proceedings of the First International Conference KR89. (1989) 11. Wessel, M.: Obstacles on the way to spatial reasoning with description logics - some undecidability results. In Proceedings of the International Workshop on Description Logics 2001 (DL 2001), CEUR Workshop Proceedings. Volume 49., (2001)