=Paper=
{{Paper
|id=None
|storemode=property
|title=Elimination of Complex RIAs without Automata
|pdfUrl=https://ceur-ws.org/Vol-846/paper_21.pdf
|volume=Vol-846
|dblpUrl=https://dblp.org/rec/conf/dlog/Simancik12
}}
==Elimination of Complex RIAs without Automata==
https://ceur-ws.org/Vol-846/paper_21.pdf
Elimination of Complex RIAs without Automata
František Simančík
Department of Computer Science, University of Oxford, UK
Abstract. We present an algorithm that eliminates complex role inclusion ax-
ioms (RIAs) from a SROIQ ontology preserving all logical consequences not
involving non-simple roles. Unlike other existing methods, our algorithm does
not explicitly construct finite automata recognizing the languages generated by
the RIAs. Instead, it is formulated as a recursive expansion of universal restric-
tions, similar to well-known encodings of transitivity axioms.
1 Introduction
Complex role inclusion axioms (RIAs) R1 ◦ . . . ◦ Rn v R are an important feature
by which the web ontology language OWL 2 [2], based on the description logic (DL)
SROIQ [5], extends the earlier standard OWL DL. Unrestricted use of complex RIAs
causes undecidability of the basic reasoning tasks already in case of fairly inexpres-
sive DLs and modal logics such as ALC [1]; decidability is recovered by requiring that
RIAs, when viewed as context-free grammar rules R → R1 . . . Rn , generate regular
languages [3, 4, 7]. However, checking if a given set of RIAs has this property is already
difficult; this problem is related to checking regularity of pure context-free grammars
[10] (which do not distinguish terminal and non-terminal symbols) whose decidability
appears to have been long open [7]. To avoid this difficulty, a stronger syntactic regular-
ity condition that requires RIAs to be acyclic (apart from a few selected cases such as
transitivity axioms) is imposed in SROIQ. This condition is easy to check and allows
for an effective construction of the underlying finite automata [5].
The standard automata construction for SROIQ [5] is an inductive procedure that
performs non-trivial manipulations such as taking the mirrored copy and the disjoint
union of previously constructed automata. To implement the procedure directly, de-
velopers of OWL 2 reasoners have to either look for suitable third-party libraries that
support such operations, or resort to writing their own automata library. In this paper,
we present an algorithm that eliminates complex RIAs from a SROIQ ontology with-
out explicitly using finite automata. Instead, our algorithm is formulated as a simple
recursive expansion of universal restrictions, similar to well-known encodings of tran-
sitivity axioms, using acyclicity of RIAs directly to ensure termination. For this reason,
we believe that our method might be easier to implement in practice. Furthermore, we
illustrate that, by introducing new rules for handling universal restrictions, the tableau
algorithm for SROIQ [5] can be modified to apply our elimination on the fly. In that
case, no pre-construction due to complex RIAs is needed at all.
Our recursive expansion of universal restrictions is inspired by and directly simu-
lates the recursion in the standard automata construction. Therefore, for many purposes,
the result of our elimination algorithm can be regarded as equivalent to the standard
automata-based encoding [6].
2 Preliminaries
2.1 The DL SROIQ
For a gentle introduction to DLs we refer the readers to the DL primer [8]. In this section
we merely recall the definition (syntax only) of SROIQ [5], together with the notions
of a regular RBox and of polarity of concept occurrence. We follow the approach of
Shearer [11] in assuming that the set of simple roles is given in the signature and calling
a RIA w v R complex iff R is non-simple (even if w is of length 1).
A signature Σ = hΣS , ΣR , ΣC , ΣI i consists of mutually disjoint sets of atomic
roles ΣR , atomic concepts ΣC , and individuals ΣI , together with a distinguished sub-
set ΣS ⊆ ΣR of simple atomic roles. The set of roles (over Σ) is R := ΣR ∪
{R− | R ∈ ΣR }; the set of simple roles is S := ΣS ∪ {S − | S ∈ ΣS }. A role chain
is an expression of the form R1 · . . . · Rn with n ≥ 1 and each Ri ∈ R. The function
inv(·) is defined on roles by inv(R) := R− and inv(R− ) := R where R ∈ ΣR , and
extended to role chains by inv(R1 · . . . · Rn ) := inv(Rn ) · . . . · inv(R1 ).
The set C of SROIQ concepts (over Σ) is defined recursively as follows:
C := ΣC | {ΣI } | (C u C) | (C t C) | ¬C | ∃R.C | ∀R.C | >n S.C | 6n S.C | ∃S.Self .
A role inclusion axiom (RIA) is either a simple RIA of the form S1 v S2 where
S1 , S2 ∈ S, or a complex RIA of the form w v R where w is a role chain and
R ∈ R \ S. A role assertion is an axiom of the form Ref(R) (reflexivity), Irr(S) (ir-
reflexivity), Uni(R) (universality), or Dis(S1 , S2 ) (role disjointness), where R ∈ R and
S(i) ∈ S. Transitivity and symmetry must be expressed as R · R v R and inv(R) v R
respectively. An RBox is a finite set of RIAs and role assertions.
A regular order ≺ is an irreflexive transitive binary relation on the set of roles R
satisfying R1 ≺ R2 iff inv(R1 ) ≺ inv(R2 ). An RBox R is ≺-regular if each RIA in R
is of one of the following forms:
(R1) R1 · . . . · Rn v R with Ri ≺ R for all 1 ≤ i ≤ n;
(R2) R · R1 · . . . · Rn v R with Ri ≺ R for all 1 ≤ i ≤ n;
(R3) R1 · . . . · Rn · R v R with Ri ≺ R for all 1 ≤ i ≤ n;
(R4) R · R v R;
(R5) inv(R) v R.
An RBox R is regular if it is ≺-regular for some regular order ≺. For a regular RBox
R, let ≺R be the intersection of all regular orders ≺ such that R is ≺-regular; the depth
of R is the maximal n for which there exists a sequence R1 ≺R . . . ≺R Rn . It is easy to
show that if R is regular, then it is ≺R -regular.
A TBox is a finite set of general concepts inclusions (GCIs) of the form C v D
where C, D ∈ C. To keep the presentation simple, we do not allow ABox assertions;
these can be expressed as GCIs using nominals. A SROIQ ontology (over Σ) is a pair
O = hR, T i where R is a regular RBox and T a TBox.
Polarities of occurrences of SROIQ concepts in concepts and GCIs are defined in-
ductively as follows: C occurs positively in C. If C occurs positively (resp. negatively)
in C 0 , then C occurs positively (resp. negatively) in C 0 u D, D u C 0 , C 0 t D, D t C 0 ,
∃R.C 0 , ∀R.C 0 , >n R.C 0 , and D v C 0 , and C occurs negatively (resp. positively) in
¬C 0 , 6n R.C 0 , and C 0 v D.
2.2 Conservative Encodings
We use the framework of conservative extensions [9] to prove correctness of our encod-
ing of RIAs. Let O be an ontology over a signature Σ = hΣS , ΣR , ΣC , ΣI i, and let Q
be an ontology over a (not necessarily strictly) larger signature. Then Q is a conserva-
tive encoding of O (also Q is conservative over O) if
(i) for every model I of O there exists a model J of Q such that I and J have the
same domain and coincide on the interpretation of ΣR , ΣC , and ΣI , and
(ii) for every model J of Q there exists a model I of O such that I and J have the
same domain and coincide on the interpretation of ΣR , ΣC , and ΣI .
Since this definition is sensitive to Σ, to avoid ambiguity, we will assume that each on-
tology carries its signature with it, so that each ontology is over only one signature. The
signature may, however, contain symbols not occurring in the ontology. Note that, un-
like the standard notion of a conservative extension, the above notion of a conservative
encoding does not require that Q contains all axioms from O.
We define a simple-conservative encoding analogously except that the models I
and J are only required to coincide on ΣS , ΣC , and ΣI . As observed by Lutz et al.
[9], this model-theoretic notion of conservativity implies that the two ontologies en-
tail the same consequences over ΣS , ΣC , and ΣI . We will prove that our encoding of
complex RIAs produces a simple-conservative encoding of the input ontology. Thus,
in particular, the two ontologies have the same classification (ignoring the extra atomic
concepts introduced in the encoding). Furthermore, by introducing new concept defini-
tions A ≡ C and B ≡ D in the original ontology, one can check subsumptions even
between concepts C and D which contain non-simple roles.
2.3 Languages Generated by RIAs
Each RIA w v R can be expressed equivalently as inv(w) v inv(R); to avoid having to
keep this in mind, let Rc := R∪{inv(w) v inv(R) | w v R ∈ R} be the completion of
the RBox R. Note that R and Rc are equivalent and R is ≺-regular iff Rc is ≺-regular.
The languages LR (R) are defined inductively by (i) R ∈ LR (R) for each role
R, and (ii) if R1 · . . . · Rn v R ∈ Rc and wi ∈ LR (Ri ) for all 1 ≤ i ≤ n, then
w1 · . . . · wn ∈ LR (R). Intuitively, LR (R) is the language generated from the role R
by the grammar rules {R → w | w v R ∈ Rc }. Horrocks et al. [5] showed that if R is
regular, then each LR (R) is a regular language, the finite automata recognizing LR (R)
can be effectively constructed by induction over ≺R , and the size of these automata is
at most exponential in the depth of R.
An interpretation function ·I is extended to the languages LR (R) as follows:
LR (R)I = {hx, yi | there exists w ∈ LR (R) such that hx, yi ∈ wI }. (1)
One can easily prove by induction on the definition of LR (R) that w ∈ LR (R) implies
R |= w v R. The following proposition is a direct consequence of this fact.
Proposition 1. If I |= R, then LR (R)I = RI .
3 Motivation
In this section we motivate and present (first approximation of) our RIA-elimination
algorithm. For simplicity, we do not yet consider symmetry axioms (R5) in this section.
Many SROIQ constructors are restricted to simple roles and therefore do not in-
teract with complex RIAs. The key step in eliminating complex RIAs is to capture
the propagation of universal restrictions over non-simple roles. Consider the following
property:
if x ∈ (∀R.C)I and hx, yi ∈ LR (R)I , then y ∈ C I . (2)
Every model I of the RBox R satisfies (2) simply because LR (R)I = RI by Propo-
sition 1, in which case (2) coincides with semantics of universal restrictions. The main
idea behind all methods for dealing with complex RIAs (e.g., [4–6]) is to axiomatise
(using a finite number of GCIs) the property (2) for all ∀R.C occurring in the ontology,
and use this axiomatisation to simulate the presence of complex RIAs from R.
In the simplest case, when all RIAs in R are of the form (R1), this can be achieved
by a simple recursive expansion of all universal restrictions occurring in the ontology.
To expand ∀R.C, for each RIA R1 · . . . · Rn v R ∈ Rc introduce the axiom
∀R.C v ∀R1 .∀R2 . . . ∀Rn .C, (3)
and recursively expand all the nested universal restrictions on the right-hand side of (3).
If all RIAs are of the form (R1), then Ri ≺R R for each role Ri in (3), so the depth of
the recursion is bounded by the depth of R and the expansion terminates.
In case there are other forms of RIAs in R, e.g., transitivity axioms, the recursion
would never terminate. On the other hand, transitivity axioms can be eliminated using
several well-known encodings. For example, to capture (2) for the concept ∀R.C with
respect to the transitivity axiom R · R v R, introduce two new atomic concepts I and
F not in the signature of the the ontology and assert
∀R.C v I, F v C, I v ∀R.F, F v I. (4)
This encoding is inspired by the fact that the RIA R · R v R generates the regular
language R+ which is recognised by the following finite automaton:
start i f
R
The encoding simulates the run of this automaton from all instances of ∀R.C in a model
of (4). Concepts I and F respectively correspond to the initial state i and the final state
f , the first axiom initialises the automaton at all x ∈ (∀R.C)I , the second axiom
ensures that y ∈ C I for all y in the final state, and the last two axioms encode the tran-
sitions of the automaton. This method generalises easily to all cases when the language
LR (R) is given by a finite automaton [6].
We propose a RIA-elimination algorithm that does not assume that the automaton
is already fully constructed. Our method recursively expands all universal restrictions
similarly to (3), but uses a two-state automaton at each step to handle the cyclic forms
of RIAs similarly to (4). More specifically, to expand the universal restriction ∀R.C,
introduce two new atomic concepts I and F , assert
(E0) ∀R.C v I, F v C, and I v ∀R.F ,
(E1) I v ∀R1 . . . . ∀Rn .F for each RIA R1 · . . . · Rn v R ∈ Rc of form (R1);
(E2) F v ∀R1r . . . . ∀Rnr .F for each RIA R · R1r · . . . · Rnr v R ∈ Rc of form (R2),
(E3) I v ∀R1l . . . . ∀Rnl .I for each RIA R1l · . . . · Rnl · R v R ∈ Rc of form (R3),
(E4) F v I if R · R v R ∈ Rc ,
and recursively expand all the universal restrictions introduced in (E1)–(E3), but not
the ∀R.F introduced in (E0). Regularity of R ensures that the depth of the recursion is
bounded by the depth of R. This encoding is inspired by the following automaton (the
-edge is present iff R · R v R ∈ Rc ) used in the construction by Horrocks et al. [5]
that recognises the language generated from R by the RIAs referred to in (E1)–(E4) :
start i f
R
R1l . . . Rnl R1 . . . Rn R1r . . . Rnr
Example 1. We will now demonstrate the RIA-elimination algorithm on an example.
Let ΣS = {P, R}, ΣR = {P, R, S, T }, ΣC = {A, B, C, D}, ΣI = ∅, and let O =
hR, T i be the following ontology over the signature Σ = hΣS , ΣR , ΣC , ΣI i:
R = {T · S v T, T · T v T, R · S v S, P v R}, (5)
T = {A v D t ∀T.¬C, B v ∃T.∃P.∃S.C}. (6)
Note that R is regular and P ≺R R ≺R S ≺R T . The RIA P v R is simple; the
remaining RIAs in R are complex. To expand the universal restriction ∀T.¬C occurring
in T , introduce new atomic concepts I1 and F1 , and assert the following axioms:
∀T.¬C v I1 , F1 v ¬C, I1 v ∀T.F1 by (E0) (7)
F1 v ∀S.F1 by (E2) for T · S v T (8)
F1 v I 1 by (E4) for T · T v T (9)
Then, to recursively expand the new universal restriction ∀S.F1 occurring in (8), intro-
duce new atomic concepts I2 and F2 , and assert the following axioms:
∀S.F1 v I2 , F2 v F1 , I2 v ∀S.F2 by (E0) (10)
I2 v ∀R.I2 by (E3) for R · S v S (11)
Finally, since we intend to keep all simple RIAs in the RBox and the role R is sim-
ple, the new universal restriction ∀R.I2 introduced in (11) does not need to be further
expanded. Let U be the TBox consisting of the new axioms (7)–(11). The results of
the next section will establish that the ontology Q = h{P v R}, T ∪ Ui is simple-
conservative over O, so, in particular, the two ontologies entail the same consequences
over ΣS , ΣC , and ΣI . For example, both O and Q entail P v R and A u B v D.
Note that this cannot be strengthened to all consequences over Σ since, for example, O
entails T · P · S v T and B v ∃T.C, but Q does not entail either of these axioms.
4 The RIA-Elimination Algorithm
In this section we formally present our RIA-elimination algorithm and prove that it
produces a simple-conservative encoding of the input ontology. Some of the proofs are
rather technical, in those cases we present only brief sketches here. More detailed proofs
can be found in the appendix.
There are several important points about the algorithm that were omitted in the
previous section in favour of simplicity; this is amended in this section. Firstly, if R
is a symmetric role, i.e., inv(R) v R ∈ Rc , then the concept ∀R.C is additionally
expanded in the same way as ∀inv(R).C would be. Secondly, since we do not assume
that the ontology is in negation normal form, we have to treat negative occurrences of
existential restrictions similarly to positive occurrences of universal restrictions. Finally,
the expansion rule (E0) is inefficient because it introduces the axiom ∀R.C v I in
which ∀R.C occurs negatively. Negative occurrences of universal restrictions are not
Horn, i.e., they lead to non-determinism in reasoning. To avoid this problem, instead
of asserting ∀R.C v I, the algorithm replaces all positive occurrences of ∀R.C in the
original ontology by I. This way we obtain a Horn-preserving encoding.
To keep track of the progress of the algorithm, we label those concepts ∀R.C and
∃R.C that still need to be expanded with R as defined below.
Definition 1 (R-labelled concepts). Given an RBox R, we introduce new concept con-
structors ∀R R.C and ∃R R.C called R-labelled universals and R-labelled existentials
respectively. Their semantics is defined as follows:
(∀R R.C)I = {x | ∀y : hx, yi ∈ LR (R)I → y ∈ C I },
(∃R R.C)I = {x | ∃y : hx, yi ∈ LR (R)I ∧ y ∈ C I }.
R-labelled concepts are SROIQ concepts that may additionally contain R-labelled
universals and existentials. To distinguish them from normal SROIQ concepts, we
sometimes call the latter unlabelled. Similarly, we speak of R-labelled (resp. unla-
belled) ontologies.
Note that the semantics of R-labelled concepts is irrelevant for the execution of the
algorithm. It does, however, greatly simplify the proofs, since with this semantics we
can prove that each intermediate expansion step of the algorithm already produces a
simple-conservative encoding of the input ontology.
Given an input ontology O = hR, T i, the initial step of the algorithm is to remove
all complex RIAs from O (keeping all simple RIAs and all role assertions) and label all
positive occurrences of universal restrictions and all negative occurrences of existential
restrictions in O with R to indicate that they need to be expanded. This is defined more
formally in the following two definitions.
Definition 2 (labelling). Let R be an RBox. For x an unlabelled concept or a TBox, let
σR (x) be the result of labelling each positive occurrence of each universal restriction
and each negative occurrence of each existential restriction in x with R. Dually, let
σ̄R (x) be the result of labelling each negative occurrence of each universal restriction
and each positive occurrence of each existential restriction in x with R.
Definition 3 (initialisation). Let O = hR, T i be an unlabelled SROIQ ontology
over a signature Σ. Let Rs := R \ {w v R ∈ R | w v R is a complex RIA}. The ini-
tialisation of O is the R-labelled ontology hRs , σR (T )i over the same signature Σ.
The next theorem proves that initialisation produces a simple-conservative encod-
ing of O. This captures the intuition that positive universal restrictions and negative
existential restrictions are the only SROIQ features that interact with complex RIAs.
Theorem 1. The initialisation of O is simple-conservative over O.
Proof (sketch). We must show that (i) for each model I of O there is a model J of
Q = hRs , σR (T )i that agrees with I on ΣS , ΣC , and ΣI , and (ii) vice versa.
For (i), we show that each model I of O is already a model of Q. Trivially, I |=
R implies I |= Rs since Rs ⊆ R. By Proposition 1, we have LR (R)I = RI , so
(∀R.C)I = (∀R R.C)I and (∃R.C)I = (∃R R.C)I for all concepts ∀R.C and ∃R.C.
This means that R-labelling does not affect the interpretation of concepts in I, so I |=
T implies I |= σR (T ). Therefore I |= Q.
For (ii), each model J of Q can be transformed to a model I of O by extending
the interpretation of roles to RI = LR (R)J . From J |= Rs one proves that I and J
agree on simple roles. Checking that I |= R is routine. The key step to prove I |= T is
to show by structural induction for each unlabelled concept D that σR (D)J ⊆ DI ⊆
σ̄R (D)J ; since σR (T ) = {σ̄R (C) v σR (D) | C v D ∈ T }, we can then infer I |=
T from J |= σR (T ). Hence I |= O. t
u
After initialisation, the algorithm repeatedly expands all R-labelled universals and
existentials until it arrives at an unlabelled ontology. Before we define these expansions,
in the next definition we first introduce an auxiliary function expand(I v ∀R R.F ) that
encodes the axiom I v ∀R R.C only using universals ∀R S.D with S ≺R R. The func-
tion implements the transition function of the two-state automaton from the previous
section, and additionally deals with symmetric roles R by expanding I v ∀R R.C in
the same way as I v ∀R inv(R).C. The correctness of this encoding is expressed in the
following Proposition 2. Its proof can be found in the appendix.
Definition 4 (expand). Let R be a regular RBox, R a role, and I and F atomic con-
cepts. We define expand0 (I v ∀R R.F ) to be the set consisting of the following GCIs:
1. I v ∀R.F ,
2. I v ∀R R1 . . . ∀R Rn .F for each R1 · . . . · Rn v R ∈ Rc ,
3. F v ∀R R1 . . . ∀R Rn .F for each R · R1 · . . . · Rn v R ∈ Rc ,
4. I v ∀R R1 . . . ∀R Rn .I for each R1 · . . . · Rn · R v R ∈ Rc ,
5. F v I if R · R v R ∈ Rc ,
where each Ri is distinct from R. Finally, we define expand(I v ∀R R.F ) to be
(
expand0 (I v ∀R R.F ) ∪ expand0 (I v ∀R inv(R).F ) if inv(R) v R ∈ Rc ,
expand0 (I v ∀R R.F ) otherwise.
Proposition 2. If I |= expand(I v ∀R R.F ), then I |= I v ∀R R.F .
We are now ready to define the expansions of R-labelled concepts. Similarly to
structural transformation, ∀R -expansion uses atomic concepts I and F as new names
for the concepts ∀R R.C and C respectively, replaces all positive occurrences of ∀R R.C
by I, adds F v C, and, instead of asserting I v ∀R R.F , it uses expand(I v ∀R R.F )
to encode the same property. ∃R -expansion works similarly but it additionally uses
the equivalence of ∃R.I v F with I v ∀inv(R).F ; it uses atomic concepts I and
F as new names for the concepts C and ∃R R.C respectively, adds C v I, replaces
all negative occurrences of ∃R R.C by F , and, instead of asserting ∃R R.I v F , it uses
expand(I v ∀R inv(R).F ) to encode the same property. More formal definitions follow.
Definition 5 (substitution). For concepts Cold and Cnew , and x a concept or a TBox,
let ρ+ [Cnew / Cold ](x) resp. ρ− [Cnew / Cold ](x) be the result of simultaneously replacing
each positive resp. negative occurrence of Cold in x by Cnew .
Definition 6 (∀R - and ∃R -expansions). Let R be a regular RBox and let O = hR0 , T i
be an R-labelled ontology over a signature Σ = hΣS , ΣR , ΣC , ΣI i.
∀R -expansion:
Let ∀R R.C be an R-labelled universal occurring in O. Let I and F be two different
atomic concepts not in ΣC . The ∀R R.C-expansion of O is the ontology
hR0 , ρ+ [I / ∀R R.C](T ) ∪ {F v C} ∪ expand(I v ∀R R.F ) i.
∃R -expansion:
Let ∃R R.C be an R-labelled existential occurring in O. Let I and F be two different
atomic concepts not in ΣC . The ∃R R.C-expansion of O is the ontology
hR0 , ρ− [F / ∃R R.C](T ) ∪ {C v I} ∪ expand(I v ∀R inv(R).F ) i.
In both cases, the resulting ontology is over the signature hΣS , ΣR , ΣC ∪ {I, F }, ΣI i.
Note that the initialisation of an ontology contains only positive occurrences of
R-labelled universals and only negative occurrences of R-labelled existentials. Fur-
thermore, both expansions introduce only positive occurrences of R-labelled univer-
sals. Therefore, when used in the context of the RIA-elimination algorithm, the above
expansions will actually eliminate all occurrences of ∀R R.C resp. ∃R R.C from the
ontology. The reason for making the substitutions polarity-sensitive was to make the
following theorem hold for arbitrary ontologies.
Theorem 2. Let R be a regular RBox, let O be an R-labelled ontology, and let Q be a
∀R R.C- or ∃R R.C-expansion of O. Then Q is conservative over O.
Proof (sketch). Let O = hR0 , T1 i be an R-labelled ontology over Σ and let Q =
hR0 , T2 i be a ∀R R.C-expansion of O. We need to show that (i) for each model I of O
there exists a model J of Q that agrees with I on Σ, and (ii) vice versa.
For (i), each model I of O can be extended to a model of Q by interpreting the new
concepts I I := (∀R R.C)I and F I := (∃R inv(R).∀R R.C)I . The substitution merely
replaces some occurrences of ∀R R.C by I, and (∀R R.C)I = I I , so I |= T1 implies
I |= ρ+ [I / ∀R R.C](T1 ). To conclude that I is a model of Q, it remains to check that
I satisfies each axiom in {F v C} ∪ expand(I v ∀R R.F ). This is done using the
definition of I I and F I ; for example, I |= F v C holds because ∃R inv(R).∀R R.C v
C is a tautology. The remaining axioms can be checked similarly.
For (ii), we show that each model J of Q is already a model of O. To prove J |= T1 ,
the key step is to prove by structural induction for all concepts D over Σ that
ρ+ [I / ∀R R.C](D)J ⊆ DJ ⊆ ρ− [I / ∀R R.C](D)J ; (12)
then J |= ρ+ [I / ∀R R.C](T1 ) ⊆ T2 implies J |= T1 . The only non-trivial case in
the induction is D = ∀R R.C, where (12) reduces to I J ⊆ (∀R R.C)J ; to show this,
we apply Proposition 2 to J |= ({F v C} ∪ expand(I v ∀R R.F )) ⊆ T2 to infer
J |= I v ∀R R.C, which is equivalent to the required I J ⊆ (∀R R.C)J .
The proof of the case when Q is an ∃R R.C-expansion of O, is similar: Each model
I of O can be extended to a model of Q by interpreting I I := (∀R inv(R).∃R R.C)I
and F I := (∃R R.C)I . The substitution merely replaces some occurrences of ∃R R.C
by F , and (∃R R.C)I = F I , so I |= T1 implies I |= ρ− [F / ∃R R.C](T1 ). To conclude
that I is a model of Q, one can check that the definition of I I and F I satisfies each
axiom in {C v I} ∪ expand(I v ∀R inv(R).F ).
To show that each model J of Q is a model of O, prove by structural induction
for all concepts D over Σ that ρ− [F / ∃R R.C](D)J ⊆ DJ ⊆ ρ+ [F / ∃R R.C](D)J .
This, in the only non-trivial case D = ∃R R.C, reduces to (∃R R.C)J ⊆ F J ; to show
this, apply Proposition 2 to J |= ({C v I} ∪ expand(I v ∀R inv(R).F )) ⊆ T2 to infer
J |= C v ∀R inv(R).F , which is equivalent to the required (∃R R.C)J ⊆ F J . t
u
The following theorem is our main result. It ensures that the RIA-elimination al-
gorithm produces a simple-conservative encoding of the input ontology, and that the
number of expansions is at most exponential in the depth of R. Therefore, since each
expansion is linear in the size of R, the algorithm can be implemented to run in time
exponential in the depth of R, which is optimal since complex RIAs are known to incur
an exponential increase in the complexity of reasoning [6].
Theorem 3. Let O = hR, T i be an unlabelled SROIQ ontology, let hRs , T0 i be the
initialisation of O, and let (Ti )ni=1 be any sequence of TBoxes such that hRs , Ti+1 i is
obtained from hRs , Ti i by a ∀R - or ∃R -expansion. Then hRs , Tn i is simple-conservative
over O. Moreover, n is bounded by kT k · (2 · kRk)d where d is the depth of R.
Proof. The proof uses the observation that if O1 is simple-conservative over O, and O2
is conservative over O1 , then O2 is also simple-conservative over O, which follows di-
rectly from the respective definitions. With this, it is easy to prove by induction on i that
each hRs , Ti i is simple-conservative over O: the base case is established in Theorem 1,
and the induction step follows from Theorem 2 and the above observation. Therefore,
in particular, hRs , Tn i is simple-conservative over O.
To obtain the bound on n, let r = 2 · kRk. As remarked earlier, each ∀R R.C- resp.
∃R R.C-expansion eliminates all occurrences of ∀R R.C resp. ∃R R.C from the ontol-
ogy, and introduces at most r new concepts ∀R S.D (the factor 2 is due to symmetric
roles) all satisfying S ≺R R. Therefore, each ∀R.C and ∃R.C occurring in O (of which
there are at most kT k) can altogether generate at most 1 + r + r2 + . . . + rd−1 < rd
R-labelled universals and existentials, which yields the required bound of kT k · rd . t u
I-intro: if ∀R.C ∈ L(x),
then L(x) += I[∀R.C], and
L(x) += I[∀inv(R).C] if inv(R) v R ∈ Rc .
F -intro: if I[∀R.C] ∈ L(x) and ( R ∈ L(x, y) or inv(R) ∈ L(y, x) ),
then L(y) += F [∀R.C].
F -elim: if F [∀R.C] ∈ L(y),
then L(y) += C.
I-exp: if I[∀R.C] ∈ L(x),
then L(x) += ∀R1 . . . ∀Rn .F [∀R.C] for each R1 · . . . · Rn v R ∈ Rc , and
L(x) += ∀R1 . . . ∀Rn .I[∀R.C] for each R · R1 · . . . · Rn v R ∈ Rc .
F -exp: if F [∀R.C] ∈ L(y),
then L(y) += ∀R1 . . . ∀Rn .F [∀R.C] for each R1 · . . . · Rn · R v R ∈ Rc , and
L(y) += I[∀R.C] if R · R v R ∈ Rc .
Fig. 1. Tableau rules for expansion of complex RIAs
Finally, as already observed in Example 1, the algorithm can be optimised by re-
placing all concepts ∀R S.C and ∃R S.C with a simple role S directly by ∀S.C and
∃S.C respectively, omitting their expansion. Interestingly, this makes the algorithm
work without further modifications even in the presence of arbitrary cyclic simple RIAs;
it is enough that complex RIAs are acyclic to ensure termination.
5 Elimination of Complex RIAs in the Tableau Algorithm
In this section we briefly sketch how the tableau algorithm for SROIQ [5] can be mod-
ified to perform our encoding of complex RIAs on the fly. We assume that the readers
are already familiar with the tableau algorithm. We use the standard notation L(x) and
L(x, y) for labels of nodes and edges in the completion graph. We assume that with
each concept ∀R.C we can uniquely associate new concepts I[∀R.C] and F [∀R.C];
these will be used in the expansion of ∀R.C. Since the tableau algorithm operates with
concepts in negation normal form, it can never encounter a negative occurrence of an
existential restriction, therefore expansion is only applicable to universal restrictions.
To obtain the modified tableau algorithm, replace all rules relating to universal re-
strictions (rules ∀1 , ∀2 , ∀3 in [5]) by the rules in Fig. 1, where L(x) += C is a shorthand
for L(x) := L(x) ∪ {C} and each Ri is implicitly distinct from R. These rules can be
readily compared to the expansion rules (E0)–(E4) from Section 3: rules I-intro, F -
intro, and F -elim implement the axioms ∀R.C v I, I v ∀R.F , and F v C of (E0),
rule I-exp implements the expansions (E1) and (E3), and rule F -exp implements the
expansions (E2) and (E4). The rules can be extended with blocking conditions as usual.
Note that the first three rules together subsume the standard ∀-rule, but additionally
introduce I[∀R.C] in L(x) and F [∀R.C] in L(y), even in case there are no complex
RIAs in the ontology at all. To eliminate this overhead, similarly to the optimisation
above, one can restrict rule I-intro to non-simple roles R, and apply the standard ∀-rule
to universal restrictions with simple roles.
6 Conclusions
We presented an algorithm that encodes complex RIAs in SROIQ without construct-
ing finite automata. The algorithm can also be applied in weaker DLs: apart from GCIs
involving atomic concepts and concepts already occurring in the ontology, the algo-
rithm introduces only GCIs of the form I v ∀R.F where I and F are atomic concepts,
and R a possibly inverse role. Inverse roles are not strictly required either: if desired,
each I v ∀R− .F with an inverse role R− can be replaced by the equivalent ∃R.I v F .
Our algorithm shares many theoretical properties of the traditional approaches based
on automata, e.g., it is Horn-preserving and runs in time exponential in the depth of the
RBox. On the other hand, a notable difference between the two approaches is that, in the
automata construction, one can apply standard techniques for minimising the number
of automata states and thus potentially reduce the number of new concepts introduced
in the encoding. While it might be difficult to provide similarly robust optimisation
for our algorithm, several simple optimisations, such as the one presented here that
restricts expansion of universal restrictions to non-simple roles, might already help in
many realistic cases. Experimental evaluation of the algorithm is left for future work.
References
1. Baldoni, M., Giordano, L., Martelli, A.: A tableau calculus for multimodal logics and some
(un)decidability results. In: Proc. of the Int. Conf. on Automatic Reasoning with Analytic
Tableaux and Related Methods (TABLEAUX 1998). pp. 44–59. Springer (1998)
2. Cuenca Grau, B., Horrocks, I., Motik, B., Parsia, B., Patel-Schneider, P., Sattler, U.: OWL 2:
The next step for OWL. Journal of Web Semantics 6(4), 309–322 (2008)
3. Demri, S., Nivelle, H.D.: Deciding regular grammar logics with converse through first-order
logic. Journal of Logic, Language and Information 14(3), 289–329 (2005)
4. Goré, R., Nguyen, L.A.: A tableau calculus with automaton-labelled formulae for regular
grammar logics. In: Proc. of the Int. Conf. on Automatic Reasoning with Analytic Tableaux
and Related Methods (TABLEAUX 2005). pp. 138–152. Springer (2005)
5. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Proc. of the 10th
Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2006). pp. 57–67.
AAAI Press (2006)
6. Kazakov, Y.: RIQ and SROIQ are harder than SHOIQ. In: Proc. of the 11th Int. Conf.
on Principles of Knowledge Representation and Reasoning (KR 2008). pp. 274–284. AAAI
Press (2008)
7. Kazakov, Y.: An extension of complex role inclusion axioms in the description logic SROIQ.
In: Proc. of the 5th Int. Joint Conf. on Automated Reasoning (IJCAR 2010). pp. 472–486.
Springer (2010)
8. Krötzsch, M., Simančík, F., Horrocks, I.: A description logic primer. CoRR abs/1201.4089
(2012), http://arxiv.org/abs/1201.4089
9. Lutz, C., Walther, D., Wolter, F.: Conservative extensions in expressive description logics.
In: Proc. of the 20th Int. Joint Conf. on Artificial Intelligence (IJCAI 2007). pp. 453–458.
AAAI Press (2007)
10. Maurer, H.A., Salomaa, A., Wood, D.: Pure grammars. Information and Control 44(1), 47–72
(1980)
11. Shearer, R.: Scalable Reasoning for Description Logics. Ph.D. thesis, University of Oxford
(2010)