We investigate cases where an ontology expressed in a seemingly hard DL can be polynomially reduced to one in a simpler logic, while preserving reasoning outcomes for classi cation and fact entailment. Our transformations target the elimination of inverse roles, universal and existential restrictions, and in the best case allow us to rewrite the given ontology into one of the OWL 2 pro les. Even if an ontology cannot be fully rewritten into a pro le, in many cases our transformations allow us to exploit further optimisation techniques. Moreover, the elimination of some out-of-pro le axioms can improve the performance of modular reasoners, such as MORe. We have tested our techniques on both classi cation and data reasoning tasks with encouraging results.
State-of-the-art DL reasoners such as Pellet [
However, notwithstanding extensive research into optimisation techniques, DL reasoning remains a challenge in practice. Indeed, the aforementioned evaluation also revealed that many ontologies are still hard for reasoners to classify. Furthermore, due to the high worst-case complexity of reasoning, systems are inherently not robust, and even minor changes to ontologies can have a signi cant e ect on performance. Finally, the limitations of DL reasoners become even more apparent when reasoning with ontologies and large datasets.
These issues have motivated a growing interest in lightweight DLs: weaker
logics that enjoy more favourable computational properties. Among these are
the OWL 2 pro les [
This paper extends our results in [
In this paper, we propose techniques to (at least partially) rewrite ontologies in the direction of the OWL 2 pro les, speci cally EL and RL. All rewritings are polynomial and preserve classi cation and fact entailment.
In Section 3, we consider rewritings that are applicable to SHOIQ [
In Section 4, we focus on Horn ontologies and consider rewritings into OWL 2 RL. The RL pro le is tightly connected to Datalog, and hence existential restrictions 9R:C occurring positively in axioms are disallowed, unless C is a singleton nominal f g
o . We show that when R ful lls certain conditions, such concepts 9R:C can be rewritten into existential restrictions over nominals as accepted in OWL 2 RL; we call such roles R reuse-safe. In the limit case where all roles are reuse-safe, the ontology can be polynomially rewritten into RL; if, additionally, the ontology contains no cardinality constraints, it can also be rewritten into EL. Furthermore, if only some roles are reuse-safe, they can be treated by (hyper-)tableau reasoners in an optimised way, potentially reducing the size of the constructed pre-models and improving reasoning times.
Our experiments over a large ontology repository reveal that our techniques can lead to substantial improvements in classi cation times for both standard and modular reasoners. Furthermore, we show that many ontologies contain only reuse-safe roles and hence can be fully rewritten into RL; thus, highly scalable RL triple stores can be exploited for large-scale data reasoning. 2
A signature consists of disjoint countable sets of individuals NI, atomic concepts
NC and atomic roles NR. A role is an element of NR [ fR jR 2 NRg. The
function Inv( ) is de ned over roles as follows, where R 2 NR: Inv(R) = R and
Inv(R ) = R. An RBox R is a nite set of RIAs R v R0 and transitivity axioms
Tra(R), with R and R0 roles. We denote with vR the minimal relation over roles
in R s.t. R vR S and Inv(R) vR Inv(S) hold if R v S 2 R. We de ne vR as the
re exive-transitive closure of vR. A role R is transitive in R if there is a role S
such that S vR R, R vR S and either Tra(S) 2 R or Tra(Inv(S)) 2 R. A role
R is simple in R if no transitive role S exists s.t. S vR R. The set of SHOIQ
concepts is the smallest set containing A 2 NC, >, ?, fog (nominal), :C
(negation), C u D (conjunction), C t D (disjunction), 9R:C (existential restriction),
8R:C (universal restriction), 6 nS:C (at-most restriction), and > nR:C (at-least
restriction), for A 2 NC, C and D SHOIQ concepts, o 2 NI, R a role and S a
simple role, and n > 0. A literal concept is either atomic or the negation of an
atomic concept. A TBox T is a nite set of GCIs C v D with C; D concepts.
An ABox A is a nite set of assertions C(a) (concept assertion), R(a; b) (role
assertion), a b (equality assertion), and a 6 b (inequality assertion), with C a
concept, R a role and a; b individuals. A fact is either a concept assertion A(a)
with A atomic, a role assertion, an equality assertion, or an inequality assertion.
An ontology is a triple O = (R; T ; A). The semantics is standard [
We assume familiarity with standard conventions for naming DLs, and we just provide here a de nition of the OWL 2 pro les. A SHOIQ ontology is: { EL if (i) it does not contain inverse roles, negation (other than ?), disjunction, at-most restrictions and at-least restrictions; and (ii) every universal restriction appears only in a GCI of the form > v 8R:C. { RL if each GCI C v D satis es (i) C does not contain negation as well as universal, at-least, and at-most restrictions; (ii) D does not contain negation (other than ?), union, existential restrictions (other than of the form 9R:fog), at-least restrictions, and at-most restrictions with n > 1. { QL if it does not contain transitivity and for each GCI C v D (i) C is either atomic or 9R:>; (ii) D is of the form dn i=1 Bi with each Bi either a literal concept, or ?, or of the form 9R:A with R a role and A either atomic or >. Classi cation of O is the task of computing all subsumptions O j= A v B with A 2 NC [ f>g, and B 2 NC [ f?g. Fact entailment is to check whether O j= , for a fact. Both problems are reducible to ontology unsatis ability. 3
In this section, we propose techniques for transforming non-EL axioms into EL. Whenever possible, inverse roles are replaced with fresh symbols and the ontology is extended with axioms simulating their possible e ects. At the same time, we attempt to transform positive occurrences of universal restrictions into negative occurrences of existential restrictions while inverting the relevant role. Preprocessing Our rst step is to bring O into a suitable normal form. Normalisation facilitates further rewriting steps, and allows us to identify syntactically non-EL axioms which have a direct correspondence in EL.
De nition 1. A normalised GCI is of the form: dn j=1 Dj , where each i=1 Ci v Fm Ci is one of >, A, or 9R:A, and each Dj is one of ?, A, f g o , 9R:A, 9R:fog, 8R:A, or 6 kR:B, with A (B) an atomic (literal) concept, R a role, o 2 NI , and k > 1; each concept Ci (resp. Dj ) is said to occur positively (negatively) in the GCI. An ontology O = (R; T ; A) is normalised if A only contains facts and each GCI in T is normalised. Furthermore, O is Horn if m = 1 for each GCI in O and each at-most restriction 6 kR:C satis es k = 1.
Proposition 1. There exists a polynomial transformation over SHOIQ ontologies O such that: (i) (O) is normalised; (ii) O is satis able i (O) is satis able; and (iii) if O is EL (resp. RL, or QL), then so is (O).3 3Under a trivial relaxation of QL syntax. Please see the technical report for details. x B a A
NR x B b)
R y C Inverse Rewritability Satis ability of SHOIQ ontologies is NExpTimecomplete, whereas for SHOQ it is ExpTime-complete; thus, in general, inverse roles cannot be faithfully eliminated from SHOIQ ontologies by a polynomial transformation. The following example illustrates that an obstacle to rewritability is the interaction between inverses and at-most restrictions.
Example 1. Consider O = (R; T ; A), with R = ;, A = fA(a)g, and T as follows:
T = fA v 9R :B; B v 9R:C; B v 6 1 R:>g Note that O j= C(a). In every model ( I ; I ), object aI must be R -connected to some x 2 BI (due to the rst axiom in T ); also, x must be R-connected to some y 2 CI (due to the second axiom). Then, for the last axiom to be satis ed, aI and y must be identical; thus, aI 2 CI . Figure 1 a) depicts such a model. Consider now O0 obtained from O by replacing R with a fresh atomic role NR . Then, O0 6j= C(a), and Fig. 1 b) depicts a model of O0 not satisfying C(a). Extending O0 with EL axioms to simulate the interaction between inverses and cardinality restrictions (and recover the missing entailment) seems infeasible. }
We next propose su cient conditions for inverse roles to be rewritable. De nition 2. Let O = (R; T ; A) be a normalised SHOIQ ontology. A (possibly inverse) role R is generating in O, if an existential restriction over a role R0 vR R occurs positively in a GCI.
An inverse role S in O is rewritable if for each X 2 fS; S g occurring in at-most restrictions in O we have that Inv(X) is not generating in O. Intuitively, roles in positive occurrences of existential restrictions are those \inducing" the edges between individuals and their successors in a canonical forest model; a role R is generating if it is a super-role of one such R0. Our condition ensures that \backwards" edges in such a canonical model of O (i.e., those induced by an inverse role) cannot invalidate an at-most cardinality restriction. As we will show later on (c.f. Theorems 1 and 2), when all inverse roles in a SHOIQ ontology are rewritable we can faithfully rewrite the ontology into SHOQ by means of a polynomial transformation.
C v D t 8R:A ) fC v D t X, 9Inv(R):X v Ag
if R is not generating C v D t 8R:A ) fC v D t X, 9Inv(R):X v A, X v 8R:Ag
if Inv(R) is generating and R is generating C u 9R:A v D ) fC u X v D; A v 8Inv(R):Xg
if Inv(R) is generating and R is not generating C u 9R:A v D ) fC u X v D, A v 8Inv(R):X, 9R:A v Xg
if Inv(R) is generating and R is generating
The Transformation Before presenting our transformation formally, we exemplify how universal restrictions can be replaced with (negative occurrences of) existential restrictions if the relevant roles are not generating. Example 2. Consider O = (R; T ; A) where R = fR v S g, A = fA(a); S(a; b)g, and T = fA v 8S:B; B v 9R:C; 9S:B v D; C u D v ?g.
Clearly, O is unsatis able. Furthermore, it does not contain at most restrictions, and hence S is rewritable. We rst extend O with logically redundant axioms, which make explicit information that may be lost when replacing inverses with fresh symbols. Thus, we extend T with 9S :A v B, and B v 8S :D; furthermore, we extend R with R v S; and nally, A with the assertion S (b; a).
An important observation is that S is not generating. As a result, we can dispense with axiom A v 8S:B. Then we replace S with a fresh symbol NS and R with NR . The resulting O0 = (R0; T 0; A0) is as follows: R0 = fR v NS ; NR v Sg T 0 = f9NS :A v B; B v 9R:C; 9S:B v D; B v 8NS :D; C u D v ?g A0 = fA(a); S(a; b); NS (b; a)g O0 is unsatis able; furthermore it is in EL except for axiom B v 8NS :D. This axiom cannot be dispensed with since S is generating, and hence it is needed to propagate information along NS -edges in a canonical model. }
We next present our transformation. For simplicity, we restrict ourselves to ALCHOIQ ontologies; later on, we discuss issues associated with transitivity axioms and show how our techniques extend to SHOIQ.
De nition 3. Let O = (R; T ; A) be a normalised ALCHOIQ ontology. The ontology (O) = (R0; T 0; A0) is obtained as follows: 1. Axiom Rewriting: the ontology Oe = (Re; Te; Ae) is de ned as follows: { Re extends R with an axiom Inv(R) v Inv(S) for each R v S in R; { Te is obtained from T by applying exhaustively the rewrite rules in Fig. 2, and deleting all axioms mentioning a non-generating role R for which A contains no assertion S(a; b) with S v R or S v Inv(R); { Ae extends A with an assertion R (b; a) for each R(a; b) 2 A. 2. Inverse Replacement: (O) = (R0; T 0; A0) is obtained from Oe by replacing each occurrence of an inverse role that is rewritable in Oe with a fresh role.
The rst step in the transformation extends the ontology with axioms that simulate the e ect of inverse roles, which are eliminated in the second step. Furthermore, the rewrite rules in Fig. 2 are designed to eliminate \harmless" occurrences of universal restrictions (see Example 2).
Theorem 1. Let O0 = (O). Then, O0 is of size polynomial in the size of O and it is satis able i O is satis able. Furthermore, if O contains only rewritable inverse roles, then O0 is an ALCHOQ ontology. Finally, if O is Horn and it satis es the following properties, then O0 is EL: 1. it does not contain at-most restrictions; 2. concepts 8R:A with R generating occur only in axioms > v 8R:A; and 3. if 9R:A occurs negatively, either A = >, or Inv(R) is not generating.
Theorem 1 identi es a class of ALCHOIQ ontologies which can be transformed into equisatis able ALCHOQ ontologies and for which standard reasoning is feasible in ExpTime (in contrast to NExpTime). This result can be exploited for optimisation: tableaux reasoners employ pairwise blocking techniques over ALCHOIQ ontologies, while they rely on more aggressive single blocking for ALCHOQ inputs, which reduces the size of the constructed pre-models.
The last condition in the theorem establishes su cient conditions on O for the transformed ontology O0 to be in EL. A simple case is when O is in the QL pro le of OWL 2, in which case the transformed ontology is guaranteed to be in EL. An interesting consequence of this result is that highly optimised EL reasoners, such as ELK, can be exploited for classifying QL ontologies.
In many cases our transformation may only succeed in partially rewriting a ontology into EL (cf. Example 2). Even in these cases, our techniques can have substantial practical bene ts (see Evaluation section). As already mentioned, in the absence of inverse roles (hyper-)tableau reasoners may exploit more aggressive blocking techniques. Furthermore, modular reasoning systems such as MORe, which are designed to behave better for ontologies with a large EL subset, bene t from our transformations.
Dealing with Transitivity Axioms The transformation in De nition 3 is not applicable to ontologies with transitivity axioms.
Example 3. Consider O = (R; T ; A) with R = fR v R ; Tra(R)g, A = fA(a)g, and T = fA v 9R:B; A v C; 9R :C v Dg. Let O0 = (O), where we assume that the transitivity axiom Tra(R) stays unmodi ed in O0. More precisely, A0 = A, R0 = fR v NR ; NR v R; T ra(R)g, and T 0 = fA v 9R:B; A v C; 9NR :C v D; C v 8R:Dg. Then, O j= D(a), but O 6j 0 = D(a); An attempt to recover this entailment by making NR transitive does not solve the problem.} To address this issue, we eliminate transitivity before applying our transformation in De nition 3. We consider that ontologies are further normalised s.t. each GCI has at most one negative occurrence of an existential restriction or one positive occurrence of a universal restriction over a non-simple role. We say that such an ontology is transitivity-normalised.
De nition 4. Let O = (R; T ; A) be a transitivity normalised SHOIQ ontology.Let (O) = (R0; T 0; A) be an ontology in which R0 is obtained from R by removing all transitivity axioms and T 0 is obtained from T by adding: { for each axiom C v D t 8R:A in T , with R non-simple, and each transitive sub-role S of R: C v D t 8S:YAS , YAS v 8S:YAS , and YAS v A, where YAS is a fresh atomic concept uniquely associated to S and A; { for each axiom C u 9R:A v D in T , with R non-simple, and each transitive sub-role S of R in R: A v ZAS , 9S:ZAS v ZAS , and C u 9S:ZAS v D, where ZAS is a fresh atomic concept uniquely associated to S and A.
Lemma 1 establishes the properties of transitivity elimination, and Theorem 2 shows that our techniques extend to a SHOIQ ontology O by rst applying to O and then to the resulting ontology.
Lemma 1. Let O be a transitivity normalised SHOIQ ontology. Then:
2. (O) is a normalised ALCHOIQ ontology; furthermore,
O is Horn. 3. (O) can be computed in time polynomial in the size of O. 4. If O is EL, then so is (O). 5. If an inverse role R is rewritable in O, then it is also rewritable in (O) is Horn i (O).
Theorem 2. Let O = (R; T ; A) be a transitivity normalised SHOIQ ontology, and let O0 = ( (O)). Then, O0 satis es all properties in Theorem 1. 4
We now restrict our attention to Horn ontologies, and consider rewritings into
RL. The idea is to identify roles R such that each positive occurrence of a concept
9R:C can be replaced by an existential restriction 9R:fog over a nominal (which
is allowed in RL) and a fact C(o). We call such roles reuse-safe. It is well-known
that all roles in an EL ontology satisfy this property, and hence it is possible
to faithfully rewrite EL ontologies into RL [
B1; C s1
R
R R a A
R
R
S F s7 R
R
S
S F s8 s9 F s2 B2; C
R R
S s10 F
R F1 s11 s12 F2
F1 s17
s18 F2 : : : a)
B1; C s1
R
S
R R a A
R
R S R F s7
S
R F1 s8
s9 F2 b) s2 B2; C
R S D1; E s3 D2; E s4 s5 D1; E s6 D2; E
D1; E s3 D2; E s4 s5 D1; E s6 D2; E
Since R is generating and O has no inverses, we have (O) = O. Figure 3 a) depicts a canonical model of O. Role S is reuse-safe since it is not \a ected" by non-EL axioms involving universal restrictions. Thus, we can \fold" the model by identifying all nodes with an S-predecessor to a single fresh nominal and obtain a smaller model satisfying the same subsumptions and facts (Fig. 3 b). } De nition 5. Let O = (R; T ; A) be a normalised Horn ontology. A role R in O is reuse-safe if either no existential restriction of the form 9R:A with A 2 NC occurs positively in O, or each of the following properties hold for each role S: { R 6vR S and R 6vR Inv(S) if S occurs in a concept 6 1 S:B; { R 6vR S if O contains an axiom C v 8S:B with C 6= >; { R 6vR Inv(S) if a concept 9S:A with A 6= > occurs negatively in O. For each concept 9R:A which occurs positively in O with R reuse-safe, let cR;A be a fresh individual. Then, (O) is ontology obtained from O by replacing each such 9R:A by 9R:fcR;Ag and adding the fact B(cR;A) to A.
Theorem 3.
(O) is satis able i
In practice, system developers can achieve the same goal as our transformation by making their implementations sensitive to reuse-safe roles: to satisfy an axiom involving an existential restriction over such role, a system should reuse a suitable distinguished individual instead of generating a fresh one.
We next analyse the limit case where all roles in a Horn ontology O are reuse-safe. We show that (O) is an RL ontology. Furthermore, we can identify a new e ciently-recognisable class of DL ontologies that contains all the OWL 2 pro les, and for which standard reasoning is feasible in polynomial time. Theorem 4. For the class C of Horn ontologies for which all roles are reusesafe: 1. Checking whether a SHOIQ ontology O is in C is feasible in polynomial time; 2. Every EL, QL and RL ontology is contained in C; 3. (O) is an RL ontology for each O 2 C; and 4. Classi cation and fact entailment in C are feasible in polynomial time.
Finally, it is worth emphasising that, although the transformations in De nition 3 and in Sect. 3 are very di erent and serve rather orthogonal purposes, they are connected in the limit case where all roles are reuse-safe and the ontology does not contain cardinality restrictions.
Proposition 2. Let O be a normalised Horn ontology that does not contain at-most restrictions. Then, ( (O)) is EL i all roles in O are reuse-safe. 5
Classi cation Experiments We tested all the OWL 2 ontologies in the Oxford Ontology Repository,4 as well as a \hard" version of the FlyAnatomy ontology, and two additional ontologies from NCBO BioPortal5: BIOMODELS and CAO. Several ontologies have a small number of non-SHOIQ axioms, which we removed for testing. We measured classi cation times for the latest versions of HermiT (v.1.3.8) and MORe (v.0.1.5) using their standard settings. Experiments were performed on a laptop with 16 GB RAM and Intel Core 2.9 GHz processor running Java v.1.7.0 21, with a timeout of 1h.
EL rewriting Experiments. Out of the 793 test ontologies, we selected those 70 with inverse roles, and which HermiT takes at least 1s to classify. For each ontology O we computed a transformed version O0 (see Section 3), and have compared classi cation times for HermiT and MORe. Out of the 70 test ontologies 50 contained only rewritable inverse roles, which could be successfully eliminated using our transformations, and 10 of these could be fully rewritten into EL. HermiT and MORe exhibited very similar behaviour, and Table 1 presents results for some representative cases. Both reasoners timed out on 8 out of these 4http://www.cs.ox.ac.uk/isg/ontologies/ 5https://bioportal.bioontology.org 50 ontologies, and only on 6 of them after applying our transformations; thus, they succeeded on 2 transformed ontologies that could not be classi ed in their original form. For 41 of the remaining 42 cases, both reasoners showed either a noticeable improvement or reasoning times very close to the original ones; on average, there was an 3:74 speedup factor for HermiT and 4:37 for MORe. In the case of HermiT, improvements can be explained by the use of a more optimised blocking strategy, which decreased the size of the constructed models by X on average. The improvement in MORe was due, on the one han, to the improvement of HermiT and, on the other hand, to the use of ELK over a larger EL module. Only in one case (BIOMODELS) we observed decreased performance of 21% in HermiT and 78% in MORe. Finally, 20 of the 70 tested ontologies contain non-rewritable inverse roles. As expected, in these cases we obtained no consistent improvement since the presence of inverses forces HermiT to use pairwise blocking; furthermore, in some cases the transformation negatively impacts performance, as it adds a substantial number of axioms to simulate the e ect of inverse roles. Hence, it seems that our techniques are clearly bene cial only when all inverse roles are rewritable.
Reuse-safe experiments. From the 793 ontologies in the corpus, we identi ed 174 Horn ontologies that do not fall within any of the OWL 2 pro les. We have applied our transformation in De nition 3 to these ontologies and found that 53 do not contain unsafe roles and hence are rewritable into RL. Furthermore, in the remaining ontologies 89% of the roles were reuse-safe, on average. We have tested classi cation times with HermiT over the transformed ontologies, but found that the transformation had a negative impact on performance. This is explained by the introduction of nominals, which forces HermiT to disable anywhere blocking. As mentioned in Section 4, it would be more e ective to implement safe reuse as a modi cation of HermiT; this, however, implies non-trivial modi cations to the core of the reasoner, which is left for future work.
Data Reasoning Experiments From the 50 ontologies with rewritable inverse
roles, we selected those 30 equipped with an ABox, and performed instance
retrieval using HermiT on the original and rewritten ontologies. On average,
we observed a 3:64 speedup factor. We also tested our rewritings into RL for
the LUBM benchmark, which comes with a non-EL ontology that can be fully
rewritten into RL. For each dataset, we recorded the times needed to compute the
instances of all atomic concepts in the ontology. We compared HermiT over the
original ontology and the RL reasoner RDFox[
Several techniques for inverse role elimination in DL ontologies have been
developed. Ding et al. [
Ren at al. proposed technqiues for approximating an OWL ontology into EL
[
Our techniques in Section 4 extend the so-called combined approach to query
answering in EL [
We have proposed techniques for rewriting ontologies into the OWL 2 pro les. Our techniques are easily implementable as preprocessing steps in DL reasoners, and can lead to substantial improvements in reasoning times. Furthermore, we have established su cient conditions for ontologies to be polynomially rewritable into the EL and RL pro les. Thus, for the class of ontologies satisfying our conditions reasoning becomes feasible in polynomial time. There are many avenues to explore for future work. For example, we will investigate extensions of our EL rewriting techniques that are capable of rewriting away disjunctive axioms. Furthermore, we are planning to implement safe reuse in HermiT and evaluate the impact of this optimisation on classi cation.
Acknowledgements. Work supported by the Royal Society, the EPSRC project Score! and the National Science Foundation under the award TROn: Tractable Reasoning with Ontologies. 23. Tsarkov, D., Horrocks, I.: FaCT++ Description Logic reasoner: System description. In: IJCAR. pp. 292{297 (2006) 24. Wu, Z., Eadon, G., Das, S., Chong, E.I., Kolovski, V., Annamalai, M., Srinivasan, J.: Implementing an inference engine for RDFS/OWL constructs and user-de ned rules in Oracle. In: ICDE. pp. 1239{1248 (2008) 25. Zhou, Y., Cuenca Grau, B., Horrocks, I., Wu, Z., Banerjee, J.: Making the most of your triple store: query answering in OWL 2 using an RL reasoner. In: WWW (2013)