=Paper=
{{Paper
|id=Vol-477/paper-8
|storemode=property
|title=An Extension of Regularity Conditions for Complex Role Inclusion Axioms
|pdfUrl=https://ceur-ws.org/Vol-477/paper_68.pdf
|volume=Vol-477
|dblpUrl=https://dblp.org/rec/conf/dlog/Kazakov09
}}
==An Extension of Regularity Conditions for Complex Role Inclusion Axioms==
<pdf width="1500px">https://ceur-ws.org/Vol-477/paper_68.pdf</pdf>
<pre>
      An Extension of Regularity Conditions for
          Complex Role Inclusion Axioms

                                Yevgeny Kazakov

                     Oxford University Computing Laboratory



1     Introduction
The description logic (DL) SROIQ [1] provides a logical foundation for the
new version of the web ontology language OWL 2.1 In comparison to the DL
SHOIN which underpins the first version of OWL,2 SROIQ provides several
new constructors for classes and axioms. One of the new powerful features of
SROIQ are so-called complex role inclusion axioms (RIAs) which allow for
expressing implications between role chains and roles R1 · · · Rn v R. It is well-
known that unrestricted usage of such axioms can easily lead to undecidability for
modal and description logics [2–5], with a notable exception of the DL EL++ [6].
Therefore certain syntactic restrictions are imposed on RIAs in SROIQ to regain
decidability. Specifically, the restrictions ensure that RIAs R1 · · · Rn v R when
viewed as production rules for context-free grammars R → R1 . . . Rn induce a
regular language. In fact, the tableau-based reasoning procedure for SROIQ [1]
does not use the syntactic restrictions directly, but takes as an input the resulting
non-deterministic finite automata for RIAs. This means that it is possible to
use exactly the same procedure for any set of RIAs for which the corresponding
regular automata can be constructed.
    Unfortunately, the syntactic restrictions on RIAs in SROIQ are not satisfied
in all cases when the language induced by the RIAs is regular. In fact, it is not
possible to come up with such a most general syntactic restriction since, given a
context-free grammar, it is in general not possible to determine whether it defines
a regular language (see, e.g., [7]). In this paper we analyse several common use
cases of RIAs which correspond to regular languages but cannot be expressed
within SROIQ. We then propose an extension of the syntactic restrictions for
RIAs, which can capture such cases. Our restrictions have several nice properties,
which could allow for their seamless integration into future revisions of OWL:
 1. Our restrictions are conservative over the restrictions in SROIQ. That is,
    every set of RIAs that satisfies the restriction in SROIQ will automatically
    satisfy our restrictions.
 2. Our restrictions can be verified in polynomial time in the size of RIAs.
 3. Our restrictions are constructive, which means that there is a procedure that
    builds the corresponding regular automaton for every set of RIAs that satisfy
    our restrictions.
1
    http://www.w3.org/TR/owl2-syntax/
2
    http://www.w3.org/TR/owl-ref/
             Name                      Syntax    Semantics
                           Concepts
             atomic concept               A      AI (given)
             nominal                     {a}     {aI }
             top concept                  >      ∆I
             negation                    ¬C      ∆I \ C I
             conjunction               C uD      C I ∩ DI
             existential restriction    ∃R.C     {x | RI (x, C I ) 6= ∅}
             min cardinality           >nS.C     {x | ||S I (x, C I )|| ≥ n}
             exists self               ∃S.Self   {x | hx, xi ∈ S I }
                            Axioms
             complex role inclusion    ρvR         ρI ⊆ R2I
             disjoint roles         Disj(S1 , S2 ) S1I ∩ S2I = ∅
             concept inclusion        CvD          C I ⊆ DI
             concept assertion         C(a)        aI ∈ C I
             role assertion           R(a, b)      ha, bi ∈ RI
                   Table 1. The syntax and semantics of SROIQ




4. Finally, for any set of RIAs that induce a regular language, there exists
   a set of RIAs (containing possibly new roles) that satisfies our syntactic
   restrictions and preserves the semantics of the old roles. This means that
   unlike the restrictions in SROIQ, our syntactic restrictions allow to express
   any regular complex role inclusion properties.


2   Preliminaries

In this section we introduce syntax and semantics of the DL SROIQ [1]. A
SROIQ vocabulary consists of countably infinite sets NC of atomic concepts,
NR of atomic roles, and NI of individuals. A SROIQ role is either r ∈ NR ,
an inverse role r− with r ∈ NR , or the universal role U . A role chain is a
sequence of roles ρ = R1 · · · Rn , n ≥ 0, where Ri 6= U , 1 ≤ i ≤ n; when n = 0,
ρ is called the empty role chain and is denoted by . With ρ1 ρ2 we denote the
concatenation of role chains ρ1 and ρ2 , and with ρR (Rρ) we denote the role chain
obtained by appending (prepending) R to ρ. We denote by Inv(R) the inverse
of a role R defined by Inv(R) := r− when R = r, Inv(R) = r when R = r− , and
Inv(R) = U when R = U . The inverse of a role chain ρ = R1 · · · Rn is a role
chain Inv(ρ) := Inv(Rn ) · · · Inv(R1 ).
    The syntax and semantics of SROIQ is summarised in Table 1. The set of
SROIQ concepts is recursively defined using the constructors in the upper part
of the table, where A ∈ NC , C, D are concepts, R, S roles, a an individual, and
n a positive integer. A SROIQ ontology is a set O of axioms listed in the lower
part of Table 1, where ρ is a role chain, R(i) and S(i) are roles, C, D concepts,
and a, b individuals.
    A regular order on roles is an irreflexive transitive binary relation ≺ on roles
such that R1 ≺ R2 iff Inv(R1 ) ≺ R2 . A (complex) role inclusion axiom (RIA)
R1 · · · Rn v R is said to be ≺-regular, if either: (i) n = 2 and R1 = R2 = R, or
(ii) n = 1 and R1 = Inv(R), or (iii) Ri ≺ R for 1 ≤ i ≤ n, or (iv) R1 = R and
Ri ≺ R for 1 < i ≤ n, or (v) Rn = R and Ri ≺ R for 1 ≤ i < n. It is assumed
that all RIAs in O are regular for some order ≺.
    Given an ontology O, let Ō be the extension of O with RIAs Inv(ρ) v Inv(R)
for every ρ v R ∈ O. Let ρ vO R be the smallest relation between role chains and
roles such that: (i) R vO R for every role R, and (ii) ρ vO R and ρ1 Rρ2 v R0 ∈ Ō
implies ρ1 ρρ2 vO R0 .
Lemma 1. Given an ontology O, role chain ρ, and role R, it is possible to decide
in polynomial time whether ρ vO R.
Proof. We define a context-free grammar with terminal symbols sR and non-
terminal symbols AR for every role R, and production rules AR → sR for every
role R and AR → AR1 . . . ARn for every RIA R1 · · · Rn v R ∈ Ō. It is easy
to show that AR → sR1 . . . sRn w.r.t. this grammar iff R1 · · · Rn vO R. Since
the word problem (membership in the language) for context-free grammars is
decidable in polynomial time (see, e.g. [8]), then so is the property ρ vO R. t
                                                                              u
    A role S is simple (w.r.t. O) if ρ vO S implies ρ = R for some role R. It is
required that all roles S(i) in Table 1 are simple w.r.t. O. Other constructors and
axioms of SROIQ such as disjunction, universal restriction, role (ir)reflexivity,
and role (a)symetry can be expressed using the given ones.
    The semantics of SROIQ is defined using interpretations. An interpretation
is a pair I = (∆I , ·I ) where ∆I is a non-empty set called the domain of the
interpretation and ·I is the interpretation function, which assigns to every A ∈ NC
a set AI ⊆ ∆I , to every r ∈ NR a relation rI ∈ ∆I × ∆I , and to every a ∈ NI an
element aI ∈ ∆I . The interpretation is extended to roles by U I = ∆I × ∆I and
(r− )I = {hx, yi | hy, xi ∈ rI }, and to role chains by (R1 · · · Rn )I = R1I ◦ · · · ◦ RnI
where ◦ is the composition of binary relations. The empty role chain  is interpreted
by I = {hx, xi | x ∈ ∆I }.
    The interpretation of concepts is defined according to the right column of the
upper part of Table 1, where δ(x, V ) for δ ⊆ ∆I × ∆I , V ⊆ ∆I , and x ∈ ∆I
denotes the set {y | hx, yi ∈ δ ∧ y ∈ V }, and ||V || denotes the cardinality of a
set V ⊆ ∆I . An interpretation I satisfies an axiom α (written I |= α) if the
respective condition to the right of the axiom in Table 1 holds; I is a model of
an ontology O (written I |= O) if I satisfies every axiom in O. We say that α is
a (logical) consequence of O or is entailed by O (written O |= α) if every model
of O satisfies α.

3    Regularity of Role Inclusion Axioms
Given an ontology O, for every role R, we define a language LO (R) consisting of
role chains (viewed as finite words over roles) as follows:
                                LO (R) := {ρ | ρ vO R}                                 (1)
We say that the set of RIAs of O is regular if the language LO (R) is regular
for every role R. It has been shown in [1] that ≺-regularity for RIAs implies
regularity. The converse of this property, however, does not always hold, as we
demonstrate in the following example.

Example 1. Consider an ontology O consisting of the RIAs (2)–(4) below:

                               isProperPartOf v isPartOf                          (2)
                           isPartOf · isPartOf v isPartOf                         (3)
                    isPartOf · isProperPartOf v isProperPartOf                    (4)

RIAs (2)–(4) express properties of parthood relations isPartOf and isProperPartOf:
axiom (2) says that isProperPartOf is a sub-relation of isPartOf; axiom (3) says
that isPartOf is transitive; finally, axiom (4) says that if x is a part of y which is
a proper part of z, then x is a proper part of z. Since any role chain consisting
of isPartOf and isProperPartOf can be rewritten to isPartOf by applying axioms
(2) and (3), it is easy to see that:

                   LO (isPartOf) = (isPartOf | isProperPartOf)+                   (5)

Since isProperPartOf is implied only by axiom (4), it is easy to see that:

        LO (isProperPartOf) = (isPartOf | isProperPartOf)∗ · isProperPartOf       (6)

    Thus, the languages LO (isPartOf) and LO (isProperPartOf) induced by RIAs
(2)–(4) are regular. However, there is no ordering ≺ for which axioms (2)–(4) are
≺-regular. Indeed, by conditions (i)–(v) of ≺-regularity, it follows from (2) that
isProperPartOf ≺ isPartOf, and from (4) that isPartOf ≺ isProperPartOf, which
contradicts the fact that ≺ is a transitive irreflexive relation.
    In fact, there is no SROIQ ontology O that could express properties (2)–(4)
using ≺-regular RIAs. It is easy to show by induction over the definition of vO
that if the RIAs of O are ≺-regular, then R1 · · · Rn vO R implies that for every
i with 1 ≤ i ≤ n, we have either Ri = R, or Ri = Inv(R), or Ri ≺ R. This
means that for every role R, the language LO (R) can contain only words over
R, Inv(R), or R0 with R0 ≺ R. Clearly, this is not possible if LO (isPartOf) and
LO (isProperPartOf) contain the languages defined in (5) and (6).

    Axioms such as (2)–(4) in Example 1 naturally appear in ontologies describing
parthood relations, such as those between anatomical parts of the human body.
For example, release 7 of the GRAIL version of the Galen ontology3 contains the
following axioms that are analogous to (2)–(4):

                   isNonPartitivelyContainedIn v isContainedIn                    (7)
                  isContainedIn · isContainedIn v isContainedIn                   (8)
    isNonPartitivelyContainedIn · isContainedIn v isNonPartitivelyContainedIn     (9)
3
    http://www.opengalen.org/
Complex RIAs such as (7)–(9) are used in Galen to propagate properties over
chains of various parthood relations. For example, the next axiom taken from
Galen expresses that every instance of body structure contained in spinal canal
is a structural component of nervous system:
          BodyStructure u ∃isContainedIn.SpinalCanal
                                                                                 (10)
                             v ∃isStructuralComponentOf.NervousSystem
    Recently, complex RIAs over parthood relations have been proposed as an
alternative to SEP-triplet encoding [9]. The SEP-triplet encoding was introduced
[10] as a technique to enable the propagation of some properties over parthood
relations, while ensuring that other properties are not propagated. For example,
if a finger is defined as part of a hand, then an injury to a finger should be
classified as an injury to the hand, however, the amputation of a finger should
not be classified as an amputation of the hand. The SEP-triplet encoding does
not use the parthood relations explicitly, but simulates them via inclusion axioms
between special triplets of classes. Every primary class U gives rise to a triplet of
classes consisting of the structure class US describing all parts of U including U
itself, the entity class UE that is equivalent to U , and the part class UP describing
the proper parts of U . Thus the axioms FingerE v FingerS , FingerP v FingerS ,
as well as HandE v HandS , HandP v HandS describe the relations between the
classes within the triples, and one can use the axiom FingerS v HandP to express
that finger is a proper part of hand. Several drawbacks of this encoding was
mentioned and it had been argued that the explicit usage of the parthood relations
can reduce the complexity of the ontology and at the same time eliminate the
potential problems [9]. Thus, the axiom stating that finger is a proper part of
hand can be written in this setting directly as follows:
                          Finger v ∃isProperPartOf.Hand                          (11)
The explicit usage of parthood relation requires, however, complex RIAs such
as (2)–(3), which do not satisfy ≺-regularity conditions of SROIQ. This would
not be a problem for ontologies expressible within the tractable DL EL++ [6]
such as SNoMed CT,4 since EL++ does not require regularity for RIAs. But
it could be a problem when an expressivity beyond EL++ is required, such as
for translating the Galen ontology into OWL 2. In this paper we propose an
extension of regularity conditions, which, in particular, can handle axioms such
as (2)–(3).
    Another situation where ≺-regularity is too restrictive, is when “sibling
relations” between elements having common parents are to be expressed. Such
relations appear, for example, when speaking about parts that belong to the
same vehicle. The sibling relations can be expressed using the following RIAs:
                         isChildOf · isChildOf − v isSiblingOf                   (12)
                       isSiblingOf · isSiblingOf v isSiblingOf                   (13)
                         isSiblingOf · isChildOf v isChildOf                     (14)
4
    http://www.ihtsdo.org/
It can easily be shown that properties (12)–(14) could not be expressed us-
ing ≺-regular RIAs since this would require that isChildOf ≺ isSiblingOf and
isSiblingOf ≺ isChildOf. On the other hand, they induce regular languages:
    LO (isSiblingOf) = ((isChildOf · isChildOf − ) | isSiblingOf)+             (15)
                                               −                ∗
      LO (isChildOf) = ((isChildOf · isChildOf ) | isSiblingOf) · isChildOf    (16)
In the next section, we demonstrate how our extended regularity conditions can
capture such kind of axioms as well.

4   Stratified Role Inclusion Axioms
Definition 1. A preorder (a transitive reflexive relation) - on roles is said
to be admissible for an ontology O if: (i) ρ1 Rρ2 v R0 ∈ O implies R - R0 ,
and (ii) R - R0 implies Inv(R) - Inv(R0 ). We write R1 h R2 if R1 - R2 and
R2 - R1 , and R1 ≺ R2 if R1 - R2 and not R2 - R1 .
Definition 2. Let O be an ontology and - and admissible preorder for O. We
say that RIA ρ v R0 is stratified w.r.t. O and -, if for every R h R0 such
that ρ = ρ1 Rρ2 , there exist R1 and R2 such that ρ1 R vO R1 , R1 ρ2 vO R0 ,
Rρ2 vO R2 , and ρ1 R2 vO R0 . We say that O is stratified w.r.t - if every RIA
ρ v R such that ρ vO R is stratified w.r.t. O and -. We often omit “w.r.t. O”
and “w.r.t. -” if O and - are clear from the context.
Definition 3. We say that a RIA ρ1 Rρ2 v R0 is an overlap of two RIAs
ρ1 R1 v R10 and R2 ρ2 v R20 (w.r.t. O) if either (i) R = R1 , R10 vO R2 , and
R20 = R0 , or (ii) R = R2 , R20 vO R1 , and R10 = R0 . In cases (i) and (ii) we also
say that the RIAs ρ1 R1 v R10 and R2 ρ2 v R20 overlap (w.r.t O).
   In the next lemma recall that Ō is the extension of O with RIAs Inv(ρ) v Inv(R)
such that ρ v R ∈ O.
Lemma 2. Let O be an ontology and - an admissible preorder for O. Then O
is stratified w.r.t. - if and only if:
1. Every RIA in O (and hence in Ō) is stratified w.r.t. O and -;
2. Every overlap of two RIAs in Ō is stratified w.r.t O and -.
Proof. The “only if” direction of the lemma follows immediately from the defini-
tion of a stratified ontology.
    For proving the “if” direction of the lemma, without loss of generality we
may assume that whenever ρ1 Rρ2 v R0 ∈ O with R h R0 , then either ρ1 or ρ2 is
empty. Indeed, by Condition 1 of the lemma, there exist R1 such that ρ1 R vO R1
and R1 ρ2 vO R0 . Hence by removing ρ1 Rρ2 v R0 from O we preserve the relation
vO and the conditions of the lemma.
    We prove that ρ0 vO R00 implies that ρ0 v R00 is stratified w.r.t. O and -.
The proof is by two-fold induction: the outermost induction is over the length
of ρ0 , the innermost induction is over the proof of ρ0 vO R00 according to the
definition of vO . Pick an arbitrary R in ρ0 such that R h R00 . The following
cases match all possible ways of deriving ρ0 vO R00 using the definition of vO :
 – ρ0 = R00 = R. In this case R00 v R00 is trivially stratified.
 – ρ0 = ρ01 ρ1 ρ02 Rρ03 such that ρ1 vO R1 and ρ01 R1 ρ02 Rρ03 v R00 ∈ Ō.
   In this case, by Condition 1 of the lemma, ρ01 R1 ρ02 Rρ03 v R00 is stratified. Thus,
   there exist R10 and R20 such that ρ01 R1 ρ02 R vO R10 , R10 ρ03 vO R00 , Rρ03 vO R20 ,
   and ρ01 R1 ρ02 R20 vO R00 . Since ρ1 vO R1 , we have found R10 and R20 such that
   ρ01 ρ1 ρ02 R vO R10 , R10 ρ03 vO R00 , Rρ03 vO R20 , and ρ01 ρ1 ρ02 R20 v R00 .
 – ρ0 = ρ01 Rρ02 ρ2 ρ03 such that ρ2 vO R2 and ρ01 Rρ02 R2 ρ03 vO R00 . This case is
   analogous to the previous case.
 – ρ0 = ρ01 ρ1 Rρ2 such that ρ1 Rρ2 vO R0 , ρ01 R0 v R00 ∈ Ō, and ρ1 is not empty.
   Since ρ1 Rρ2 vO R0 is a subproof of ρ0 v R00 , by the induction hypothesis,
   ρ1 Rρ2 v R0 is stratified. Since R h R0 h R00 , there exist R1 and R2 such
   that ρ1 R vO R1 , R1 ρ2 vO R0 , Rρ2 vO R2 , and ρ1 R2 vO R0 . In particular,
   since R1 ρ2 vO R0 and ρ01 R0 v R00 ∈ Ō, we have ρ01 R1 ρ2 vO R00 . Since ρ1 is
   not empty, ρ01 R1 ρ2 is shorter than ρ0 = ρ01 ρ1 Rρ2 . Hence, by the induction
   hypothesis, ρ01 R1 ρ2 v R00 is stratified. Since R h R10 h R00 , there exists R10
   such that ρ01 R1 vO R10 and R10 ρ2 vO R00 . Thus, we have found R10 and R2
   such that ρ01 ρ1 R vO R10 , Rρ2 vO R2 , R10 ρ2 vO R00 , and ρ01 ρ1 R2 vO R00 .
 – ρ0 = ρ1 Rρ2 ρ02 such that ρ1 Rρ2 vO R0 , R0 ρ02 v R00 ∈ Ō, and ρ02 is not empty.
   This case is analogous to the previous case.
 – ρ0 = ρ01 Rρ2 ρ02 such that Rρ2 vO R2 , R2 ρ02 v R20 ∈ Ō, ρ02 is not empty,
   R20 vO R0 , and ρ01 R0 v R00 ∈ Ō.
   In this case RIAs ρ01 R2 ρ02 v R00 is an overlap of two RIAs R2 ρ02 v R20 and
   ρ01 R0 v R00 in Ō. Hence, by Condition 2 of the lemma, ρ01 R2 ρ02 v R00 is
   stratified. Since R h R2 h R00 , there exists R1 such that ρ01 R2 vO R1 and
   R1 ρ02 vO R00 . In particular, since Rρ2 vO R2 and ρ01 R2 vO R1 , we have
   ρ01 Rρ2 vO R1 . Since ρ02 is not empty, ρ01 Rρ2 is shorter than ρ0 = ρ01 Rρ2 ρ02 .
   Hence, by the induction hypothesis, ρ01 Rρ2 vO R1 is stratified. Since R h
   R1 h R00 , there exists R10 such that ρ01 R vO R10 and R10 ρ2 vO R1 . Thus we
   have found R10 and R0 such that ρ01 R vO R10 , R10 ρ2 ρ02 vO R00 , Rρ2 ρ02 vO R0 ,
   and ρ01 R0 vO R00 .
 – ρ0 = ρ01 ρ1 Rρ02 such that ρ1 R vO R1 , ρ01 R1 v R10 ∈ Ō, ρ01 is not empty,
   R10 vO R0 , and R0 ρ02 v R00 ∈ Ō. This case is analogous to the previous case.
 – ρ0 = ρ01 R or ρ0 = Rρ02 . This case is trivial.                                    t
                                                                                      u

Lemma 3. Given an ontology O it is possible to decide in polynomial time in
the size of O whether O is stratified.

Proof. By Lemma 2, it is sufficient to show that every RIA in O is stratified
and every overlap of two RIAs is stratified. Hence there are only polynomially
many RIAs to test. In order to test whether ρ1 Rρ2 v R0 is stratified for R,
we enumerate all possible roles R10 and R20 and check whether ρ1 R vO R10 ,
R10 ρ2 v R0 , Rρ2 vO R20 , and ρ1 R20 vO R0 . By Lemma 1, each of these conditions
can be checked in polynomial time.                                              t
                                                                                u

    Now, as we have an algorithm for deciding whether an ontology is stratified, it
is easy to see that every ontology that satisfies the original ≺-regularity conditions
for RIAs, is automatically stratified for the ordering - defined by R1 - R2 if
either R1 = R2 , or R1 = Inv(R2 ), or R1 ≺ R2 . Indeed, the only overlap between
≺-regular RIAs can occur between axioms ρ1 R1 v R1 of type (v) and axioms
R2 ρ2 v R2 of type (iv) when R1 = R2 or R1 = Inv(R2 ), which can easily be
shown to be stratified since R1 vO R2 and R2 vO R1 in these cases.
    Our next goal is to show that the set of RIAs in stratified ontologies is always
regular. Fix an ontology O and an admissible preorder - for O such that O is
stratified w.r.t. O. Define the level of a role R w.r.t. - as follows:

 – If there is no R0 such that R0 ≺ R, then the level of R is 0;
 – Otherwise the level of R is the maximum over the levels of R0 ≺ R plus 1.

    The level of a RIA ρ v R is the level of R. We write ρ ≺O R0 if R ≺O R0
for every R in ρ. As in the proof of Lemma 2, without loss of generality, we
can assume that for every RIA ρ1 Rρ2 v R0 ∈ O with R h R0 , either ρ1 or ρ2 is
empty. Hence there are four types of RIAs in Ō possible:

 – Type 0: ρ v R0 , where ρ ≺ R0 ;
 – Type 1: R1 ρ v R0 , where R1 h R0 and ρ ≺ R0 ;
 – Type 2: ρR2 v R0 , where R2 h R0 .

   Note that RIAs of the form R v R0 with R h R0 are of both Types 1 and 2.
   One nice property of stratified ontologies is that for proving ρ vO R one can
apply the RIAs in Ō in some particular order, namely: (i) apply RIAs in the
non-decreasing order of their levels, (ii) for the same level, apply the RIAs in
the non-decreasing order of their types. To formalize this strategy, we introduce
a notion of stratified proof :

Definition 4. Given an ontology O, we define the relations vin,O , 0 ≤ i ≤ 2,
n ≥ 0 between role chains and roles by induction on n ≥ 0 as follows:

1. If ρ v R0 ∈ Ō has Type 0 and level n, then ρ v0n,O R0 ;
2. If role R has level n, then R vin,O R, i = 1, 2;
3. If ρ1 v1n,O R1 and R1 ρ v R0 ∈ Ō has Type 1 and level n, then ρ1 ρ v1n,O R0 ;
4. If ρ2 v2n,O R2 and ρR2 v R0 ∈ Ō has Type 2 and level n, then ρρ2 v2n,O R0 ;
5. If ρ vin,O R and ρ1 Rρ2 vjm,O R0 with (n, i) <lex (m, j) then ρ1 ρρ2 vjm,O R0 ;

where (n, i) <lex (m, j) if either n < m, or n = m and i < j. We say that a RIA
ρ v R0 has a stratified proof in O if ρ vin,O R0 , for some n and i (0 ≤ i ≤ 2).

Lemma 4. For every stratified ontology O, if ρ0 vO R00 then ρ0 v R00 has a
stratified proof in O.

Proof (Sketch). We repeatedly apply the following transformation to the proof
of ρ0 vO R00 , which tries to swap the RIAs in Ō applied in the wrong order:
    For every overlap ρ1 Rρ2 v R0 of RIAs ρ1 R v R1 and R2 ρ2 v R0 of Types 2
and 1 in the proof of ρ0 vO R00 , where R1 vO R2 , and ρ1 and ρ2 are non-empty,
we take R20 such that R1 ρ2 vO R20 and ρ1 R20 vO R0 , which exists since O is
stratified, and replace the sub-proof of ρ1 Rρ2 v R0 in ρ0 vO R00 with the proof
using R1 ρ2 vO R20 and ρ1 R20 vO R0 ;
    This transformation always terminates. Indeed, after each transformation
step, either the number of axioms R1 · · · Rn v R0 with n ≥ 2 used in the proof
increases (when the proof of the overlap is replaced with a longer proof), or,
otherwise, the number of such axioms remains the same, but the number of pairs
(ρ1 R v R1 , R2 ρ2 v R0 ) of RIAs respectively of Types 2 and 1 such that ρ1 and ρ2
are non-empty and ρ1 R v R1 is used in the proof before R2 ρ2 v R0 , decreases.
    After the transformation terminates, it is easy to see that the proof becomes
stratified.                                                                       t
                                                                                  u
Theorem 1. For every stratified ontology O and role R one can construct an
automaton for LO (R) which is at most exponential in the level of R in O.
Proof (Sketch). By Lemma 4 for every ρ ∈ LO (R), the RIA ρ v R has a stratified
proof. It is easy to show that the language generated by RIAs of the same level
n and the same type is regular. This is a consequence of the fact that the RIAs
of Types 1 and 2 of the same level correspond to left-linear and right-linear
grammars respectively, which generate regular languages. The RIAs ρ v R0 of
Type 0 correspond to finite languages since the level of the roles in ρ is smaller
than the level of R0 , and therefore, only one step rewritings are possible. Now
the fact that LO (R) generated by RIAs of all levels is regular, follows from
the fact that regular languages are closed under substitution. The size of the
automaton for every level is at most polynomial in the size of O; thus the size of
the automaton for LO (R) is at most exponential in the level of R.              t
                                                                                u
   Returning to Example 1, we can show that the set of RIAs (2)–(4) is stratified.
Indeed, it can be shown that RIAs (3)–(4) can result in the following overlaps:

                     isPartOf · isPartOf · isPartOf v isPartOf                 (17)
              isPartOf · isProperPartOf · isPartOf v isPartOf                  (18)
              isPartOf · isPartOf · isProperPartOf v isPartOf                  (19)
              isPartOf · isPartOf · isProperPartOf v isProperPartOf            (20)

All of the above RIAs can be stratified using (2)–(4).
    On the other hand, RIAs (12)–(14) are not stratified. Indeed there are the
following overlaps between RIAs (12) and (13) and between RIAs (12) and (14):

                 isChildOf · isChildOf − · isSiblingOf v isSiblingOf           (21)
                                        −
                  isChildOf · isChildOf · isChildOf v isChildOf                (22)

The problem with (21) is that there is no R such that isChildOf − ·isSiblingOf vO R.
Intuitively, this property should hold for R = isChildOf − , but RIAs (12)–(14) are
not sufficient to derive this property. Fortunately the problem can be fixed by
declaring the role isSiblingOf to be symmetric:

                            isSiblingOf − v isSiblingOf,                       (23)
which implies: isChildOf − · isSiblingOf v isChildOf − · isSiblingOf − v (isSiblingOf ·
isChildOf)− v isChildOf − using (14). Now (12) implies that (21) is stratified.
    The problem with (22) is more involved, since isChildOf − ·isChildOf vO R does
not seem to hold for any role R introduced so far. Intuitively, by going to a child
and then going back to a parent, we should come to the “partner”—an individual
who has the same children as the initial individual. Hence we can introduce a
fresh role isPartnerOf, and add properties similar to those of isSiblingOf:

                              isChildOf − · isChildOf v isPartnerOf                            (24)
                          isPartnerOf · isPartnerOf v isPartnerOf                              (25)
                             isChildOf · isPartnerOf v isChildOf                               (26)
                                                      −
                                        isPartnerOf       v isPartnerOf                        (27)

It is now possible to show that RIAs (12)–(14) and (23)–(27) are stratified.
    It is a natural question, whether any set of RIAs that induce regular languages,
can be extended, as in the example above, to a set of RIAs that is stratified. The
following theorem gives a positive answer to this question.

Theorem 2. Let O be an ontology such that for every role R the language LO (R)
is regular. Then there exists a conservative extension O0 of O which is stratified
for every preorder - that is admissible for O.

Proof. For every role R and a role chain ρ we introduce a fresh role Rρ . We use
R as a synonym for R. For every R1 , R2 , ρ1 , ρ2 , and ρ vO R we add axioms:

                                     R1R2 ρ2 · R2ρ1 v R1ρ1 ρ2                                  (28)
                                                          ρ
                                                  vR                                          (29)

Let O0 be the extension of O with the above axioms. It is easy to show that O0 is
aSconservative extension of O: for every model I of O one can interpret (Rρ )I :=
   {(ρ0 )I | ρ0 ρ vO R} so that the axioms (28) and (29) are satisfied. Moreover, it
 can be shown that the resulting ontology is stratified. First, the original RIAs
 follow from (28) and (29): if ρ vO R for ρ = R1 R2 · · · Rn , then R1 · · · Rn v
 R1 · · · Rn v Rρ R1 · · · Rn = RR1 ···Rn R1 · · · Rn v RR2 ···Rn R2 · · · Rn v · · · v R .
 Hence by removing the original RIAs, the relation vO0 does not change. The
 remaining axioms of the form (28) and (29) are stratified, since every overlap of
 axioms (28) R1R3 ρ3 · R3R2 ρ2 · R2ρ1 v R1ρ1 ρ2 ρ3 is provable by R1R3 ρ3 · R3R2 ρ2 v R1R2 ρ2 ρ3 ,
 R1R2 ρ2 ρ3 · R2ρ1 v R1ρ1 ρ2 ρ3 , and by R3R2 ρ2 · R2ρ1 v R3ρ1 ρ2 , R1R3 ρ3 · R3ρ1 ρ2 v R1ρ1 ρ2 ρ3 .
     The only problem with O0 is that it requires infinitely many axioms (28) and
(29), since the number of new roles Rρ is not bounded. To bound the number
 of roles, we use the regularity property for languages LO (R). Define LρO (R) :=
 {ρ0 | ρ0 ρ ∈ LO (R)}, and set R1ρ1 ∼O R2ρ2 if and only if LρO1 (R1 ) = LρO2 (R2 ). By
 Myhill-Nerode theorem (see, e.g., [7]), since LO (R) is regular for each R, there
 are at most finitely many equivalence classes induced by ∼O . Since ∼O -equivalent
 roles have the same interpretations, we can identify those roles, and thus obtain
 only finitely many axioms of form (28) and (29).                                                  t
                                                                                                   u
5    Related Works and Conclusions
In this paper we have introduced a notion of stratified role inclusion axioms
which provides a syntactically-checkable sufficient condition for regularity of
RIAs—a condition that ensures decidability of SROIQ. We have demonstrated
that for every stratified SROIQ ontology, one can construct a regular automa-
ton representing the RIAs, which is worst case exponential in the size of the
ontology. The result in [11] then implies that the complexity of reasoning with
stratified SROIQ ontologies remains the same as the complexity of original
SROIQ, namely N2ExpTime-complete. Moreover, we have demonstrated that
our conditions for regularity are in a sense maximal—every ontology O with
regular RIAs can be conservatively extended to an ontology with stratified RIAs.
    Complex RIAs are closely related to interaction axioms in grammar modal
logics i1 · · · in X → i1 · · · in X [2, 12, 3]. Such axioms often cause undecid-
ability, however in [12, 3] a decidable class called the regular grammar modal
logics has been described. In [4] a decision procedure for this class is given by
a translation into the two-variable guarded fragment. Because it is in general
undecidable if the given interaction axioms are regular, the decision procedure
assumes that a regular automaton for them is also provided. When applying
these techniques to ontologies and complex RIAs, such a restriction poses a
serious practical problem: the users are unlikely to provide such automata, and
even if they do, it is in general not possible to verify if the automaton really
corresponds to the given axioms. A solution to this problem, proposed in [13, 1], is
to use a sufficient syntactical condition for regularity called ≺-regularity. Another
sufficient condition proposed in [14] requires associativity of RIAs, which means
that if R1 R2 v R10 and R10 R3 v R0 then there exists R20 such that R2 R3 v R20
and R1 R20 v R0 . It is easy to see that associativity is a partial case of our sufficient
conditions, when - is a total relation on roles. Note that Theorem 2 holds for
any preorder -, and in particular, when - is total.
    In this paper we have mainly addressed theoretical properties of ontologies
with stratified RIAs, and have argued that they can be used to model properties
which otherwise are not possible to model within SROIQ. One problem that
has not been addressed in this paper, is how to ensure that an ontology modeler
produces stratified RIAs in practice. We made a small experiment to check how
many of complex RIAs in release 7 of Galen are stratified. We found that the
total of 385 complex role inclusions in Galen produce 3604 non-stratified overlaps,
for which additional axioms are required to fix the problems. Clearly, the process
of finding the missing axioms can be very time consuming. The conditions of
stratified overlaps in such cases could provide valuable hits for finding the missing
axioms. Methods for finding stratified axioms could be one of the topics for our
future works.

References
 1. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: KR.
    (2006) 57–67
 2. del Cerro, L.F., Panttonen, M.: Grammar logics. Logique et Analyse 121-122
    (1988) 123–134
 3. Demri, S.: The complexity of regularity in grammar logics and related modal logics.
    J. Log. Comput. 11(6) (2001) 933–960
 4. Demri, S., de Nivelle, H.: Deciding regular grammar logics with converse through
    first-order logic. Journal of Logic, Language and Information 14(3) (2005) 289–329
 5. Horrocks, I., Sattler, U.: Decidability of SHIQ with complex role inclusion axioms.
    Artif. Intell. 160(1-2) (2004) 79–104
 6. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In: Proc. IJCAI-05.
    (2005) 364–369
 7. Sipser, M.: Introduction to the Theory of Computation, Second Edition. Course
    Technology (February 2005)
 8. Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and
    Computation. Addison-Wesley (1979)
 9. Suntisrivaraporn, B., Baader, F., Schulz, S., Spackman, K.A.: Replacing SEP-
    triplets in SNOMED CT using tractable description logic operators. In: AIME.
    Volume 4594 of Lecture Notes in Computer Science., Springer (2007) 287–291
10. Schulz, S., Romacker, M., Hahn, U.: Part-whole reasoning in medical ontologies
    revisited: Introducing SEP triplets into classification-based description logics. In
    Chute, C., ed.: Proc. of the 1998 AMIA Annual Fall Symposium, Hanley & Belfus
    (1998) 830–834
11. Kazakov, Y.: RIQ and SROIQ are harder than SHOIQ. In: KR, AAAI Press
    (2008) 274–284
12. Baldoni, M.: Normal Multimodal Logics: Automatic Deduction and Logic Program-
    ming Extension. PhD thesis, Università degli Studi di Torino (1998)
13. Horrocks, I., Sattler, U.: Decidability of SHIQ with complex role inclusion axioms.
    In: IJCAI. (2003) 343–348
14. Wessel, M.: Obstacles on the way to qualitative spatial reasoning with description
    logics: Some undecidability results. In: Description Logics. Volume 49 of CEUR
    Workshop Proceedings., CEUR-WS.org (2001)

</pre>