We present an algorithm that eliminates complex role inclusion axioms (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 restrictions, similar to well-known encodings of transitivity axioms.
Complex role inclusion axioms (RIAs) R1 : : : Rn v R are an important feature
by which the web ontology language OWL 2 [
The standard automata construction for SROIQ [
Our recursive expansion of universal restrictions is inspired by and directly
simulates 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 [
For a gentle introduction to DLs we refer the readers to the DL primer [
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 subset S R of simple atomic roles. The set of roles (over ) is R := R [ fR j R 2 Rg; the set of simple roles is S := S [ fS j S 2 S g. A role chain is an expression of the form R1 : : : Rn with n 1 and each Ri 2 R. The function inv( ) is defined on roles by inv(R) := R and inv(R ) := R where R 2 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 j f I g j (C u C) j (C t C) j :C j 9R:C j 8R:C j >n S:C j 6n S:C j 9S:Self : A role inclusion axiom (RIA) is either a simple RIA of the form S1 v S2 where S1; S2 2 S, or a complex RIA of the form w v R where w is a role chain and R 2 R n S. A role assertion is an axiom of the form Ref(R) (reflexivity), Irr(S) (irreflexivity), Uni(R) (universality), or Dis(S1; S2) (role disjointness), where R 2 R and S(i) 2 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 (R2) R R1 : : : Rn v R with Ri (R3) R1 : : : Rn R v R with Ri (R4) R R v R; (R5) inv(R) v R.
R for all 1
R for all 1 R for all 1 i i i n; n; n; 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 2 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 inductively as follows: C occurs positively in C. If C occurs positively (resp. negatively) in C0, then C occurs positively (resp. negatively) in C0 u D, D u C0, C0 t D, D t C0, 9R:C0, 8R:C0, >n R:C0, and D v C0, and C occurs negatively (resp. positively) in :C0, 6n R:C0, and C0 v D. 2.2
Conservative Encodings
We use the framework of conservative extensions [
Since this definition is sensitive to , to avoid ambiguity, we will assume that each ontology 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, unlike 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.
[
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[finv(w) v inv(R) j w v R 2 Rg 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 2 LR(R) for each role
R, and (ii) if R1 : : : Rn v R 2 Rc and wi 2 LR(Ri) for all 1 i n, then
w1 : : : wn 2 LR(R). Intuitively, LR(R) is the language generated from the role R
by the grammar rules fR ! w j w v R 2 Rcg. Horrocks et al. [
An interpretation function I is extended to the languages LR(R) as follows: LR(R)I = fhx; yi j there exists w 2 LR(R) such that hx; yi 2 wI g: (1) One can easily prove by induction on the definition of LR(R) that w 2 LR(R) implies R j= w v R. The following proposition is a direct consequence of this fact. Proposition 1. If I j= R, then LR(R)I = RI .
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 interact 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 2 (8R:C)I and hx; yi 2 LR(R)I , then y 2 CI :
Every model I of the RBox R satisfies (2) simply because LR(R)I = RI by
Proposition 1, in which case (2) coincides with semantics of universal restrictions. The main
idea behind all methods for dealing with complex RIAs (e.g., [
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 8R:C, for each RIA R1 : : : Rn v R 2 Rc introduce the axiom 8R:C v 8R1:8R2 : : : 8Rn:C; 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 8R: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 8R:C v I;
F v C;
I v 8R:F;
F v I: 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: (2) (3) (4) start i
R
f
The encoding simulates the run of this automaton from all instances of 8R: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 2 (8R:C)I , the second axiom
ensures that y 2 CI for all y in the final state, and the last two axioms encode the
transitions of the automaton. This method generalises easily to all cases when the language
LR(R) is given by a finite automaton [
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 8R:C,
introduce two new atomic concepts I and F , assert
(E0) 8R:C v I, F v C, and I v 8R:F ,
(E1) I v 8R1: : : : 8Rn:F for each RIA R1 : : : Rn v R 2 Rc of form (R1);
(E2) F v 8R1r: : : : 8Rnr:F for each RIA R R1r : : : Rnr v R 2 Rc of form (R2),
(E3) I v 8R1l: : : : 8Rnl:I for each RIA R1l : : : Rnl R v R 2 Rc of form (R3),
c
(E4) F v I if R R v R 2 R ,
and recursively expand all the universal restrictions introduced in (E1)–(E3), but not
the 8R: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 2 Rc) used in the construction by Horrocks et al. [
i R1l : : : Rnl
R R1 : : : Rn
f R1r : : : Rnr Example 1. We will now demonstrate the RIA-elimination algorithm on an example. Let S = fP; Rg, R = fP; R; S; T g, C = fA; B; C; Dg, I = ;, and let O = hR; T i be the following ontology over the signature = h S ; R; C ; I i: R = fT S v T;
T T v T; T = fA v D t 8T::C;
R S v S; P v Rg;
B v 9T:9P:9S:Cg: 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 8T::C occurring in T , introduce new atomic concepts I1 and F1, and assert the following axioms: F1 v :C;
I1 v 8T:F1 by (E0) by (E2) for T S v T by (E4) for T T v T 8T::C v I1; F1 v 8S:F1 F1 v I1 8S:F1 v I2;
I2 v 8R:I2 Then, to recursively expand the new universal restriction 8S:F1 occurring in (8), introduce new atomic concepts I2 and F2, and assert the following axioms: F2 v F1;
I2 v 8S:F2 by (E0) by (E3) for R S v S (10) (11) Finally, since we intend to keep all simple RIAs in the RBox and the role R is simple, the new universal restriction 8R: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 = hfP v Rg; T [ U i is simpleconservative 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 9T:C, but Q does not entail either of these axioms. (5) (6) (7) (8) (9)
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 2 Rc, then the concept 8R:C is additionally expanded in the same way as 8inv(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 8R:C v I in which 8R: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 8R:C v I, the algorithm replaces all positive occurrences of 8R: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 8R:C and 9R: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 constructors 8RR:C and 9RR:C called R-labelled universals and R-labelled existentials respectively. Their semantics is defined as follows: (8RR:C)I = fx j 8y : hx; yi 2 LR(R)I ! y 2 CI g; (9RR:C)I = fx j 9y : hx; yi 2 LR(R)I ^ y 2 CI g: 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. unlabelled) 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 n fw v R 2 R j w v R is a complex RIAg. The inis tialisation of O is the R-labelled ontology hR ; R(T )i over the same signature .
The next theorem proves that initialisation produces a simple-conservative encoding 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 j= R implies I j= Rs since Rs R. By Proposition 1, we have LR(R)I = RI , so (8R:C)I = (8RR:C)I and (9R:C)I = (9RR:C)I for all concepts 8R:C and 9R:C. This means that R-labelling does not affect the interpretation of concepts in I, so I j= T implies I j= R(T ). Therefore I j= 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 j= Rs one proves that I and J agree on simple roles. Checking that I j= R is routine. The key step to prove I j= T is to show by structural induction for each unlabelled concept D that R(D)J DI
R(D)J ; since R(T ) = f R(C) v R(D) j C v D 2 T g, we can then infer I j= T from J j= R(T ). Hence I j= O. tu
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 8RR:F ) that encodes the axiom I v 8RR:C only using universals 8RS:D with S R R. The function implements the transition function of the two-state automaton from the previous section, and additionally deals with symmetric roles R by expanding I v 8RR:C in the same way as I v 8Rinv(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 concepts. We define expand0(I v 8RR:F ) to be the set consisting of the following GCIs: 1. I v 8R:F , c 2. I v 8RR1 : : : 8RRn:F for each R1 : : : Rn v R 2 R , c 3. F v 8RR1 : : : 8RRn:F for each R R1 : : : Rn v R 2 R , c 4. I v 8RR1 : : : 8RRn:I for each R1 : : : Rn R v R 2 R ,
c 5. F v I if R R v R 2 R , where each Ri is distinct from R. Finally, we define expand(I v 8RR:F ) to be expand0(I v 8RR:F ) (expand0(I v 8RR:F ) [ expand0(I v 8Rinv(R):F ) if inv(R) v R 2 R , c otherwise: Proposition 2. If I j= expand(I v 8RR:F ), then I j= I v 8RR:F .
We are now ready to define the expansions of R-labelled concepts. Similarly to structural transformation, 8R-expansion uses atomic concepts I and F as new names for the concepts 8RR:C and C respectively, replaces all positive occurrences of 8RR:C by I, adds F v C, and, instead of asserting I v 8RR:F , it uses expand(I v 8RR:F ) to encode the same property. 9R-expansion works similarly but it additionally uses the equivalence of 9R:I v F with I v 8inv(R):F ; it uses atomic concepts I and F as new names for the concepts C and 9RR:C respectively, adds C v I, replaces all negative occurrences of 9RR:C by F , and, instead of asserting 9RR:I v F , it uses expand(I v 8Rinv(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 (8R- and 9R-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.
hR0;
+[I = 8RR:C](T ) [ fF v Cg [ expand(I v 8RR:F ) i:
hR0;
[F = 9RR:C](T ) [ fC v Ig [ expand(I v 8Rinv(R):F ) i: In both cases, the resulting ontology is over the signature h S ; R; C [ fI; F g; 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. Furthermore, both expansions introduce only positive occurrences of R-labelled universals. Therefore, when used in the context of the RIA-elimination algorithm, the above expansions will actually eliminate all occurrences of 8RR:C resp. 9RR: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 8RR:C- or 9RR:C-expansion of O. Then Q is conservative over O.
Proof (sketch). Let O = hR0; T1i be an R-labelled ontology over and let Q = hR0; T2i be a 8RR: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 II := (8RR:C)I and F I := (9Rinv(R):8RR:C)I . The substitution merely replaces some occurrences of 8RR:C by I, and (8RR:C)I = II , so I j= T1 implies I j= +[I = 8RR:C](T1). To conclude that I is a model of Q, it remains to check that I satisfies each axiom in fF v Cg [ expand(I v 8RR:F ). This is done using the definition of II and F I ; for example, I j= F v C holds because 9Rinv(R):8RR: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 j= T1, the key step is to prove by structural induction for all concepts D over that +[I = 8RR:C](D)J
DJ [I = 8RR:C](D)J ; (12) then J j= +[I = 8RR:C](T1) T2 implies J j= T1. The only non-trivial case in the induction is D = 8RR:C, where (12) reduces to IJ (8RR:C)J ; to show this, we apply Proposition 2 to J j= (fF v Cg [ expand(I v 8RR:F )) T2 to infer J j= I v 8RR:C, which is equivalent to the required IJ (8RR:C)J .
The proof of the case when Q is an 9RR:C-expansion of O, is similar: Each model I of O can be extended to a model of Q by interpreting II := (8Rinv(R):9RR:C)I and F I := (9RR:C)I . The substitution merely replaces some occurrences of 9RR:C by F , and (9RR:C)I = F I , so I j= T1 implies I j= [F = 9RR:C](T1). To conclude that I is a model of Q, one can check that the definition of II and F I satisfies each axiom in fC v Ig [ expand(I v 8Rinv(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 = 9RR:C](D)J DJ +[F = 9RR:C](D)J . This, in the only non-trivial case D = 9RR:C, reduces to (9RR:C)J F J ; to show this, apply Proposition 2 to J j= (fC v Ig [ expand(I v 8Rinv(R):F )) T2 to infer J j= C v 8Rinv(R):F , which is equivalent to the required (9RR:C)J F J . tu
The following theorem is our main result. It ensures that the RIA-elimination
algorithm 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 [
To obtain the bound on n, let r = 2 kRk. As remarked earlier, each 8RR:C- resp. 9RR:C-expansion eliminates all occurrences of 8RR:C resp. 9RR:C from the ontology, and introduces at most r new concepts 8RS:D (the factor 2 is due to symmetric roles) all satisfying S R R. Therefore, each 8R:C and 9R: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. tu I-intro: if 8R:C 2 L(x), then L(x) += I[8R:C], and c
L(x) += I[8inv(R):C] if inv(R) v R 2 R .
F -intro: if I[8R:C] 2 L(x) and ( R 2 L(x; y) or inv(R) 2 L(y; x) ),
then L(y) += F [8R:C].
F -elim: if F [8R:C] 2 L(y),
then L(y) += C.
I-exp: if I[8R:C] 2 L(x), then L(x) += 8R1 : : : 8Rn:F [8R:C] for each R1 : : : Rn v R 2 Rc, and c
L(x) += 8R1 : : : 8Rn:I[8R:C] for each R R1 : : : Rn v R 2 R .
F -exp: if F [8R:C] 2 L(y), then L(y) += 8R1 : : : 8Rn:F [8R:C] for each R1 : : : Rn R v R 2 Rc, and c L(y) += I[8R:C] if R R v R 2 R .
Finally, as already observed in Example 1, the algorithm can be optimised by replacing all concepts 8RS:C and 9RS:C with a simple role S directly by 8S:C and 9S: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
In this section we briefly sketch how the tableau algorithm for SROIQ [
To obtain the modified tableau algorithm, replace all rules relating to universal
restrictions (rules 81, 82, 83 in [
Note that the first three rules together subsume the standard 8-rule, but additionally introduce I[8R:C] in L(x) and F [8R: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 8-rule to universal restrictions with simple roles.
We presented an algorithm that encodes complex RIAs in SROIQ without constructing 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 algorithm introduces only GCIs of the form I v 8R: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 8R :F with an inverse role R can be replaced by the equivalent 9R: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.