This paper establishes the decidability of SR⊔IQ which has composition-based role Inclusion axioms (RIAs) of the form R1 ◦ · · · ◦ Rn⊑_ T1 ⊔ · · · ⊔ Tm. Also the consistency of an Abox A of SR⊔IQ DL w.r.t. Rbox R is established. Motivation for this kind of RIAs comes from applications in the eld of manufactured products as well as other conceptual modeling applications such as family relationships. The solution is based on a tableau algorithm.
Description logic (DL) [
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 [
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 = R1R2 . . . Rn.
SR⊔IQ language is an extension of SRIQ [
De nition 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 [
R1 · · · Rn ⊑˙T1 ⊔ · · · ⊔ Tm. (2)
Without additional restrictions on RIAs, some DLs [
De nition 2. Strict partial order ≺ (irreflexive, transitive, and antisymmetric),
on the set of roles, provides acyclicity [
De nition 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 [
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.
De nition 4. The semantics of the SR⊔IQ 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 CI ⊆ ∆I ; every role name R with a binary relation
RI ⊆ ∆I × ∆I and, every individual name a with an element aI ∈ ∆I [
(∃S.Self )I = {x : ⟨x, x⟩ ∈ SI }, (∀R.C)I = {x : ∀y. ⟨x, y⟩ ∈ RI ⇒ y ∈ CI }, (≥ nS.C)I = {x : ♯{y : ⟨x, y⟩ ∈ SI , y ∈ CI } ≥ n}, (≤ nS.C)I = {x : ♯{y : ⟨x, y⟩ ∈ SI , y ∈ CI } ≤ n}.
Inference problems for SR⊔IQ are defined in standard way [
De nition 6. An interpretation I satisfies a RIA R1 · · · Rn ⊑˙T1 ⊔ · · · ⊔ Tm, if R1I ◦ · · · ◦ RnI ⊆ T1I ∪ · · · ∪ TmI . An interpretation I is model of a { Tbox T (written I |= T ) if CI ⊆ 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 SI ∩ 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 ∈ CI , I |= a̸ =˙b if aI ̸= bI ,
I |= (a, b) : R if ⟨aI , bI ⟩ ∈ RI , I |= (a, b) : ¬R if ⟨aI , bI ⟩ ∈/ RI . For an interpretation I, an element x ∈ ∆I is called an instance of a concept C if x ∈ CI . 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.
De nition 7. A concept C is called satisfiable if there is an interpretation I with CI ̸= ∅. A concept D subsumes a concept C (written C ⊑˙D) if CI ⊆ 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
reduced [
The Extension of SRI Q 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(Mary) {∀hP.∀hP.(Z1 ∨ Z2)} Mary Z1 = (hGm, {W, G}, ∅) P arent1
Z2 = (hGf, {M, B}, ∅) hP
hGm
hP
Z1 ∨ Z2 x
{W, G} ⊆{ W, G, B, ¬M}
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] ⊑˙[T1 ⊔ · · · ⊔ Tm] | R1 · · · Rn ⊑˙T1 ⊔ · · · ⊔ 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 R1R2 ⊑ H1 ⊔ H2−
and S1S2 ⊑ H2− ⊔ H1 one should construct a nondeterministic finite automaton
(NFA) for role [H1 ⊔ H2−]. The automaton should accept words R1R2 and S1S2.
Namely, for every role [R] we have kept the construction of NFA B[R] based on
R′, as same as defined in [
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 arent, 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 and the individual assertion:
M ary : ∀hGm.W ⊓ ∀hGf.M ⊓ ∀hGm.G ⊓ ∀hGf.B
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 ∈ BI and (M ary, x) ∈ hGf I hold. Metalabels Z1 and Z2 are using to remember the (relevant) parts of the labels in the (3) (4) ∀B[hGm⊔hGf].(Z1 ∨ Z2). 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
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 [
In the proofs of decidability we use set P L(B[R]) = {⟨w′, q⟩ |q is a state in B[R], (∀w′′ ∈ L(B[qR]))(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′.
De nition 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 → 2NF 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 ♯ST (s, C) ≤ n,
{ (P9) if (≥ nS.C) ∈ L(s), then ♯ST (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),
{ (P14) if a̸ =˙b ∈ A, then J (a) ̸= J (b),
{ (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 ⊑ [
j0, such that Zj0 ⊆ L(s), L(s)|Qj−0 ⊆ Zˆj0 { (P6’) ∀B[R].Z ∈ L(s), where 6 Z = ∨Q∈comp([R])(Q, ZQ, ZˆQ), ZQ = L(s)|Q = {C|∀Q.C ∈ L(s)} and ZˆQ = L(s) ∩ clos(A)|Q− , for all s ∈ S and [R] ∈ R′A, { (P4a’) if ∀Bp.Z ∈ L(s), ⟨s, t⟩ ∈ E(S), and p →S q ∈ Bp, then ∀Bq.Z ∈ L(t), { (P4b’) if ∀Bp.Z ∈ L(s), ε ∈ L(Bp), and Z = ∨lj=1(Qj, Zj, Zˆj) then there is where in (P8) and (P9), ST (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, CI := {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] ∈ RA ′ , 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 S1S2 · · · 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 [
Secondly, we prove that I is model for A. We show that C ∈ L(s) implies
s ∈ CI for each s ∈ S and each C ∈ clos(A). Together with (P11)-(P14), this
implies that I is a model for A [
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 SI 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 [
(⇒) 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: SL(:s=) :∆=I {,∀JB([qRa)].Z:=|(a∃It ,∈E ∆(RI))(:∃=wR′)I∀,BL[R(]s.Z):=∈ L{C1(t∈),c⟨lwos′,(qA⟩)∈}|sP∈L(CBI[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 [
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[pR].Z ∈ L(s), ⟨s, t⟩ ∈ E (S). Assume that there is a transition
S p → q ∈ B[pR]. From definition L(s) there exists v ∈ ∆I and w′ such that ⟨w′′, q⟩ ∈ P L(B[R]) and ⟨v, t⟩ ∈ (w′′)I , so ∀B[qR].Z ∈ L(t). ∀B[R].Z ∈ L1(v), ⟨w′, p⟩ ∈ P L(B[R]) and ⟨v, s⟩ ∈ (w′)I . Let’s w′′ = w′S then For (P4b’), let’s ∀B[pR].Z ∈ L(s), ε ∈ L(B[pR]), and Z = ∨lj=1(Qj , Zj , Zˆ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 = p L(x)|Qj and Zˆj = L(x) ∩ clos(A)|Qj− . By ε ∈ B[R] we have w′ ∈ L(B[R]), so w′I ⊆ (Q1 ⊔ · · · ⊔ Ql)I , i.e. ⟨x, s⟩ ∈ (Q1 ⊔ · · · ⊔ Ql)I . This means that there is j such that ⟨x, s⟩ ∈ QI . By the rules of semantics and the definition of L(s), we j have Zj = L(x)|Qj ⊆ L(s) and L(s)|Qj− ⊆ L(x) ∩ clos(A)|Qj− = Zˆj .
De nition 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 SG(x, C) = {y|y is S − neighbour of x and C ∈ L(y)} De nition 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
no j such that L(x)|Qj− ⊆ Zˆj . { 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} ⊆ SG(x, C) with yi̸ =˙yj for all 0 ≤ i < j ≤ n, { there is ∀Bp.Z ∈ L(x), with ε ∈ L(Bp), Z = ∨lj=1(Qj , Zj , Zˆj ) and there are A completion forest that does not contain a clash is called clash-free. ⊓⊔
The blocking is employed in order to have termination [
De nition 11. A node is called blocked if it is either directly or indirectly
blocked [
In this case we say that y blocks x. A node y is indirectly blocked if one of its
ancestors is blocked [
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 algorithm 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. then L(x) → L(x) ∪{∀B[R].Z} ∀′2 If ∀Bp.Z ∈ L(x), and x is not indirectly blocked, p →S q ∈ Bp and 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, Z^j) and there is no j such that Zj ⊆ L(y) and L(y)|Qj− ⊆ Z^j then choose j such that L(y)|Qj− ⊆ Z^j and L(y) → L(y) ∪ Zj.
Proof. For the if direction, suppose that the algorithm returns ”Yes”. It means that the algorithm generated completion forest G = (V, E, L, L, ̸ =˙) without clash 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 [
p = ⟨(x0, x′0), . . . , (xn, x′n)⟩ .
For such a path, we define T ail(p) = xn and T ail′(p) = x′ . We denote the path n ⟨(x0, x′0), (x1, x′1), . . . , (xn, x′n), (xn+1, x′n+1)⟩ (5) (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 [
For the only-if direction, the proof is the same as proof in [
It is important to note that original idea of extension ALC DL with
compositionbased RIAs is presented in [