=Paper=
{{Paper
|id=Vol-1193/paper_75
|storemode=property
|title=Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs
|pdfUrl=https://ceur-ws.org/Vol-1193/paper_75.pdf
|volume=Vol-1193
|dblpUrl=https://dblp.org/rec/conf/dlog/CarralFRGHH14
}}
==Is Your Ontology as Hard as You Think? Rewriting Ontologies into Simpler DLs==
https://ceur-ws.org/Vol-1193/paper_75.pdf
Is Your Ontology as Hard as You Think?
Rewriting Ontologies into Simpler DLs ∗
David Carral1 , Cristina Feier2 , Ana Armas Romero2 , Bernardo Cuenca Grau2 ,
Pascal Hitzler1 , and Ian Horrocks2
1
Department of Computer Science, Wright State University, Dayton US
2
Department of Computer Science, University of Oxford, Oxford UK
Abstract. We investigate cases where an ontology expressed in a seem-
ingly hard DL can be polynomially reduced to one in a simpler logic,
while preserving reasoning outcomes for classification and fact entail-
ment. Our transformations target the elimination of inverse roles, uni-
versal and existential restrictions, and in the best case allow us to rewrite
the given ontology into one of the OWL 2 profiles. Even if an ontology
cannot be fully rewritten into a profile, in many cases our transforma-
tions allow us to exploit further optimisation techniques. Moreover, the
elimination of some out-of-profile axioms can improve the performance
of modular reasoners, such as MORe. We have tested our techniques on
both classification and data reasoning tasks with encouraging results.
1 Introduction
State-of-the-art DL reasoners such as Pellet [20], JFact, FaCT++ [23], RacerPro
[10], and HermiT [16] are highly-optimised for classification and have been ex-
ploited successfully in many applications. In a recent evaluation campaign, these
reasoners exhibited excellent performance on a corpus with over 1, 000 ontolo-
gies, as they were able to classify 75%-85% of the corpus in less than 10 seconds
when running on stock hardware [9,3].
However, notwithstanding extensive research into optimisation techniques,
DL reasoning remains a challenge in practice. Indeed, the aforementioned eval-
uation 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 signifi-
cant effect 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 profiles [15]. Standard reasoning tasks, such as classification and
fact entailment, are feasible in polynomial time for all profiles, and a number
of highly scalable reasoners have been developed [24,12,18,2,4]. Unfortunately,
∗
This paper extends our results in [6]. It is accompanied by a technical report which
contains all proofs (available at: http://www.cs.ox.ac.uk/isg/TR/TRsafeshoiqDL.pdf)
many ontologies fall outside the OWL 2 profiles, and we are forced to resort to
a fully-fledged reasoner if a completeness guarantee is required.
In this paper, we propose techniques to (at least partially) rewrite ontologies
in the direction of the OWL 2 profiles, specifically EL and RL. All rewritings
are polynomial and preserve classification and fact entailment.
In Section 3, we consider rewritings that are applicable to SHOIQ [11] and
that can transform non-EL axioms into EL by elimination of inverse roles and
universal restrictions. If all non-EL axioms can be rewritten, we can provide
completeness guarantees using only an EL reasoner. Otherwise, the rewritings
can still improve the performance of OWL reasoners by enabling the use of
optimisations applicable only in the absence of certain constructs and/or the
effectiveness of modular reasoners such as MORe [1].
In Section 4, we focus on Horn ontologies and consider rewritings into OWL
2 RL. The RL profile is tightly connected to Datalog, and hence existential
restrictions ∃R.C occurring positively in axioms are disallowed, unless C is a
singleton nominal {o}. We show that when R fulfills certain conditions, such
concepts ∃R.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 classification 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 Preliminaries
A signature consists of disjoint countable sets of individuals NI , atomic concepts
NC and atomic roles NR . A role is an element of NR ∪ {R− |R ∈ NR }. The func-
tion Inv(·) is defined over roles as follows, where R ∈ NR : Inv(R) = R− and
Inv(R− ) = R. An RBox R is a finite 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 ∈ R. We define v∗R as the
reflexive-transitive closure of vR . A role R is transitive in R if there is a role S
such that S v∗R R, R v∗R S and either Tra(S) ∈ R or Tra(Inv(S)) ∈ R. A role
R is simple in R if no transitive role S exists s.t. S v∗R R. The set of SHOIQ
concepts is the smallest set containing A ∈ NC , >, ⊥, {o} (nominal), ¬C (nega-
tion), C u D (conjunction), C t D (disjunction), ∃R.C (existential restriction),
∀R.C (universal restriction), 6 nS.C (at-most restriction), and > nR.C (at-least
restriction), for A ∈ NC , C and D SHOIQ concepts, o ∈ 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 finite set of GCIs C v D with C, D concepts.
An ABox A is a finite 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 [11].
We assume familiarity with standard conventions for naming DLs, and we
just provide here a definition of the OWL 2 profiles. A SHOIQ ontology is:
– EL if (i) it does not contain inverse roles, negation (other than ⊥), disjunc-
tion, at-most restrictions and at-least restrictions; and (ii) every universal
restriction appears only in a GCI of the form > v ∀R.C.
– RL if each GCI C v D satisfies (i) C does not contain negation as well as
universal, at-least, and at-most restrictions; (ii) D does not contain nega-
tion (other than ⊥), union, existential restrictions (other than of the form
∃R.{o}), at-least restrictions, and at-most restrictions with n > 1.
dnfor each GCI C v D (i) C is either
– QL if it does not contain transitivity and
atomic or ∃R.>; (ii) D is of the form i=1 Bi with each Bi either a literal
concept, or ⊥, or of the form ∃R.A with R a role and A either atomic or >.
Classification of O is the task of computing all subsumptions O |= A v B with
A ∈ NC ∪ {>}, and B ∈ NC ∪ {⊥}. Fact entailment is to check whether O |= α,
for α a fact. Both problems are reducible to ontology unsatisfiability.
3 Rewriting Ontologies into OWL 2 EL
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 effects. 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 first step is to bring O into a suitable normal form. Normal-
isation facilitates further rewriting steps, and allows us to identify syntactically
non-EL axioms which have a direct correspondence in EL.
dn Fm
Definition 1. A normalised GCI is of the form: i=1 Ci v j=1 Dj , where each
Ci is one of >, A, or ∃R.A, and each Dj is one of ⊥, A, {o}, ∃R.A, ∃R.{o},
∀R.A, or 6 kR.B, with A (B) an atomic (literal) concept, R a role, o ∈ 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 satisfies k = 1.
Proposition 1. There exists a polynomial transformation Υ over SHOIQ on-
tologies O such that: (i) Υ (O) is normalised; (ii) O is satisfiable iff Υ (O) is
satisfiable; and (iii) if O is EL (resp. RL, or QL), then so is Υ (O).3
3
Under a trivial relaxation of QL syntax. Please see the technical report for details.
R
R− NR − R
a x a x y
A, C B A B C
a) b)
Fig. 1. When rewriting away inverse roles leads to missing entailments
Inverse Rewritability Satisfiability of SHOIQ ontologies is NExpTime-
complete, 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 rewritabil-
ity is the interaction between inverses and at-most restrictions.
Example 1. Consider O = (R, T , A), with R = ∅, A = {A(a)}, and T as follows:
T = {A v ∃R− .B; B v ∃R.C; B v 6 1 R.>}
Note that O |= C(a). In every model (∆I , ·I ), object aI must be R− -connected
to some x ∈ B I (due to the first axiom in T ); also, x must be R-connected to
some y ∈ C I (due to the second axiom). Then, for the last axiom to be satisfied,
aI and y must be identical; thus, aI ∈ C I . Figure 1 a) depicts such a model.
Consider now O0 obtained from O by replacing R− with a fresh atomic role
NR− . Then, O0 6|= 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 sufficient conditions for inverse roles to be rewritable.
Definition 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 v∗R
R occurs positively in a GCI.
An inverse role S − in O is rewritable if for each X ∈ {S, S − } 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 “in-
ducing” 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 in-
duced 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 ∀R.A ⇒ {C v D t X, ∃Inv(R).X v A}
if R is not generating
C v D t ∀R.A ⇒ {C v D t X, ∃Inv(R).X v A, X v ∀R.A}
if Inv(R) is generating and R is generating
C u ∃R.A v D ⇒ {C u X v D, A v ∀Inv(R).X}
if Inv(R) is generating and R is not generating
C u ∃R.A v D ⇒ {C u X v D, A v ∀Inv(R).X, ∃R.A v X}
if Inv(R) is generating and R is generating
Fig. 2. Rewrite rules. X is fresh in each rule application.
The Transformation Before presenting our transformation formally, we ex-
emplify 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 = {R v S − }, A = {A(a); S(a, b)},
and T = {A v ∀S.B; B v ∃R.C; ∃S.B v D; C u D v ⊥}.
Clearly, O is unsatisfiable. Furthermore, it does not contain at most restric-
tions, and hence S − is rewritable. We first 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 ∃S − .A v B, and B v ∀S − .D; fur-
thermore, we extend R with R− v S; and finally, 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 ∀S.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 = {R v NS − ; NR− v S}
T 0 = {∃NS − .A v B; B v ∃R.C; ∃S.B v D; B v ∀NS − .D; C u D v ⊥}
A0 = {A(a); S(a, b); NS − (b, a)}
O0 is unsatisfiable; furthermore it is in EL except for axiom B v ∀NS − .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.
Definition 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 defined 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) ∈ 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 first step in the transformation extends the ontology with axioms that
simulate the effect 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 satisfiable iff O is satisfiable. Furthermore, if O contains only rewritable
inverse roles, then O0 is an ALCHOQ ontology. Finally, if O is Horn and it
satisfies the following properties, then O0 is EL:
1. it does not contain at-most restrictions;
2. concepts ∀R.A with R generating occur only in axioms > v ∀R.A; and
3. if ∃R.A occurs negatively, either A = >, or Inv(R) is not generating.
Theorem 1 identifies a class of ALCHOIQ ontologies which can be trans-
formed into equisatisfiable ALCHOQ ontologies and for which standard reason-
ing is feasible in ExpTime (in contrast to NExpTime). This result can be ex-
ploited 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 sufficient conditions on O for
the transformed ontology O0 to be in EL. A simple case is when O is in the
QL profile 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.
Corollary 1. If O is a normalised QL ontology, then Ξ(O) is in EL.
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 benefits (see Evaluation section). As already mentioned,
in the absence of inverse roles (hyper-)tableau reasoners may exploit more ag-
gressive blocking techniques. Furthermore, modular reasoning systems such as
MORe, which are designed to behave better for ontologies with a large EL subset,
benefit from our transformations.
Dealing with Transitivity Axioms The transformation in Definition 3 is not
applicable to ontologies with transitivity axioms.
Example 3. Consider O = (R, T , A) with R = {R v R− ; Tra(R)}, A = {A(a)},
and T = {A v ∃R.B; A v C; ∃R− .C v D}. Let O0 = Ξ(O), where we as-
sume that the transitivity axiom Tra(R) stays unmodified in O0 . More precisely,
A0 = A, R0 = {R v NR− ; NR− v R, T ra(R)}, and T 0 = {A v ∃R.B; A v
C; ∃NR− .C v D; C v ∀R.D}. Then, O |= D(a), but O0 6|= 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 transforma-
tion in Definition 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.
Definition 4. Let O = (R, T , A) be a transitivity normalised SHOIQ ontol-
ogy.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 ∀R.A in T , with R non-simple, and each transitive
sub-role S of R: C v D t ∀S.YAS , YAS v ∀S.YAS , and YAS v A, where YAS is
a fresh atomic concept uniquely associated to S and A;
– for each axiom C u ∃R.A v D in T , with R non-simple, and each transitive
S S S S
sub-role S of R in R: A v ZA , ∃S.ZA v ZA , and C u ∃S.ZA v D, where
S
ZA 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 first applying Ω
to O and then Ξ to the resulting ontology.
Lemma 1. Let O be a transitivity normalised SHOIQ ontology. Then:
1. Ω(O) is satisfiable iff O is satisfiable.
2. Ω(O) is a normalised ALCHOIQ ontology; furthermore, Ω(O) is Horn iff
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).
Theorem 2. Let O = (R, T , A) be a transitivity normalised SHOIQ ontology,
and let O0 = Ξ(Ω(O)). Then, O0 satisfies all properties in Theorem 1.
4 Rewriting Horn Ontologies into OWL 2 RL
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
∃R.C can be replaced by an existential restriction ∃R.{o} 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 [17,13,22]. Intuitively, for a role R to
be reuse-safe it must be the case that any R-edges in a canonical model of the
ontology are irrelevant to the satisfaction of non-EL axioms in the ontology.
Example 4. Consider the following ontology O = (R, T , A) where R = ∅, A =
{A(a)}, and T consists of the following axioms:
a A a A
R R R R
B1 , C s1 s 2 B2 , C B1 , C s1 s2 B2 , C
R R R R R R R R
D1 , E s3 D2 , E s4 s5 D1 , E s6 D2 , E D1 , E s3 D2 , E s4 s5 D1 , E s6 D2 , E
S S S S S S S S
F s7 F s8 s9 F s10 F F s7
R R R R R R
F1 s11 s12 F2 ... F1 s17 s18 F2 F1 s8 s 9 F2
a) b)
Fig. 3. Decreasing model size by reusing individuals as existential fillers
A v ∃R.B1 C v ∃R.D1 A v ∀R.C E v ∃S.F F v ∃R.F2 B1 u B2 v ⊥
A v ∃R.B2 C v ∃R.D2 C v ∀R.E F v ∃R.F1 F1 u F2 v ⊥ D1 u D2 v ⊥
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 “affected” 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). ♦
Definition 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 ∃R.A with A ∈ NC
occurs positively in O, or each of the following properties hold for each role S:
– R 6v∗R S and R 6v∗R Inv(S) if S occurs in a concept 6 1 S.B;
– R 6v∗R S if O contains an axiom C v ∀S.B with C 6= >;
– R 6v∗R Inv(S) if a concept ∃S.A with A 6= > occurs negatively in O.
For each concept ∃R.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 ∃R.A by ∃R.{cR,A } and adding the fact B(cR,A ) to A.
Theorem 3. Ψ (O) is satisfiable iff O is satisfiable, for each O Horn.
In practice, system developers can achieve the same goal as our transforma-
tion 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 efficiently-recognisable class of DL ontologies that contains all the OWL
2 profiles, and for which standard reasoning is feasible in polynomial time.
Ontology ID 00047 00461 00463 00470 00484 00533 00660 00760 Fly CAO
O (HermiT) 51.41 2.260 t-out 398.38 172.71 39.34 59.02 837.93 937.57 1251.46
O0 (HermiT) 29.93 1.801 422.74 75.55 50.39 20.98 11.62 402.69 10.92 197.5
O (MORe) 66.55 2.515 t-out 415.17 172.71 5.67 67.26 798.61 954.44 1220.98
O0 (MORe) 29.71 1.310 379.88 2.24 60.94 2.19 12.39 371.68 13.62 186.35
Table 1. Classification times (s) for some ontologies O and transformed versions O0 .
Theorem 4. For the class C of Horn ontologies for which all roles are reuse-
safe:
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 ∈ C; and
4. Classification and fact entailment in C are feasible in polynomial time.
Finally, it is worth emphasising that, although the transformations Ψ in Defi-
nition 3 and Ξ in Sect. 3 are very different and serve rather orthogonal purposes,
they are connected in the limit case where all roles are reuse-safe and the ontol-
ogy 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 iff all roles in O are reuse-safe.
5 Evaluation
Classification Experiments We tested all the OWL 2 ontologies in the Ox-
ford Ontology Repository,4 as well as a “hard” version of the FlyAnatomy ontol-
ogy, 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 classification 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 com-
pared classification times for HermiT and MORe. Out of the 70 test ontologies
50 contained only rewritable inverse roles, which could be successfully elimi-
nated 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
4
http://www.cs.ox.ac.uk/isg/ontologies/
5
https://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 classified 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 improve-
ment 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 pair-
wise blocking; furthermore, in some cases the transformation negatively impacts
performance, as it adds a substantial number of axioms to simulate the effect
of inverse roles. Hence, it seems that our techniques are clearly beneficial only
when all inverse roles are rewritable.
Reuse-safe experiments. From the 793 ontologies in the corpus, we identified 174
Horn ontologies that do not fall within any of the OWL 2 profiles. We have
applied our transformation in Definition 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
classification 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 effective to implement safe reuse
as a modification of HermiT; this, however, implies non-trivial modifications 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[18] over the transformed ontology.
HermiT took 3.7s for LUBM(1), and timed out for LUBM(5). In contrast RDFox
only required 0.2s for LUBM(1), 1.5s for LUBM(10), and 7.4s for LUBM(20).
These results suggest the clear benefits of transforming an ontology to RL and
exploiting highly scalable reasoners such as RDFox.
6 Related Work
Several techniques for inverse role elimination in DL ontologies have been devel-
oped. Ding et al. [8] propose a polynomial reduction from ALCI into ALC, which
is then extended in [7] to SHOI. Similarly, Song et al. [21] propose a polynomial
reduction from ALCHI to ALCH KBs to optimise classification. In all of these
approaches inverse roles are replaced with fresh symbols and new axioms are
introduced to compensate for the loss of implicit inferences. These approaches,
however, are not applicable to KBs with cardinality restrictions; furthermore,
inverse role elimination heavily relies on the introduction of universal restric-
tions, and hence they are not well-suited for rewriting into EL. Calvanese et
al. [5] propose a transformation from ALCF I knowledge bases to ALC which is
sound and complete for classification; this technique exhaustively introduces uni-
versal restrictions to simulate at-most cardinality restrictions and inverse roles,
and hence it is also not targeted towards rewritings into EL; furthermore, this
technique is not applicable to KBs with transitive roles or nominals.
Ren at al. proposed technqiues for approximating an OWL ontology into EL
[19]; such approximations are, however, incomplete and hence relevant inferences
might be lost. Finally, Lutz et al. study rewritability of first-order formulas into
EL as a decision problem [14]; the rewritings studied in [14], however, require
preservation of logical equivalence, whereas ours preserve satisfiability.
Our techniques in Section 4 extend the so-called combined approach to query
answering in EL [13,22]. They are also related to individual reuse optimisations
[17], where to satisfy existential restrictions a (hyper-)tableau reasoner tries to
reuse an individual from the model constructed thus far. Individual reuse, how-
ever, may introduce non-determinism in exchange for a smaller model: if the
reuse fails (i.e., a contradiction is derived), the reasoner must backtrack and in-
troduce a fresh individual. In contrast, in the case of reuse-safe roles reuse can
be done deterministically and hence model size is reduced without the need of
backtracking. Finally, Zhou et. al use a very similar transformation as ours to
strengthen ontologies and overestimate query answers [25]. It follows from The-
orem 4 that the technique in [25] leads to exact answers to atomic queries for
Horn ontologies where all roles are reuse-safe.
7 Conclusions and Future Work
We have proposed techniques for rewriting ontologies into the OWL 2 profiles.
Our techniques are easily implementable as preprocessing steps in DL reasoners,
and can lead to substantial improvements in reasoning times. Furthermore, we
have established sufficient conditions for ontologies to be polynomially rewritable
into the EL and RL profiles. Thus, for the class of ontologies satisfying our con-
ditions 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 classification.
Acknowledgements. Work supported by the Royal Society, the EPSRC project
Score! and the National Science Foundation under the award TROn: Tractable
Reasoning with Ontologies.
References
1. Armas Romero, A., Cuenca Grau, B., Horrocks, I.: MORe: modular combination
of OWL reasoners for ontology classification. In: ISWC. pp. 1–16 (2012)
2. Baader, F., Lutz, C., Suntisrivaraporn, B.: CEL - A polynomial-time reasoner for
life science ontologies. In: IJCAR. pp. 287–291 (2006)
3. Bail, S., Glimm, B., Gonçalves, R.S., Jiménez-Ruiz, E., Kazakov, Y., Matentzoglu,
N., Parsia, B. (eds.): Proc. of the 2nd International Workshop on OWL Reasoner
Evaluation (ORE), CEUR, vol. 1015 (2013)
4. Bishop, B., Kiryakov, A., Ognyanoff, D., Peikov, I., Tashev, Z., Velkov, R.: OWLim:
A family of scalable semantic repositories. Semantic Web J. 2(1), 33–42 (2011)
5. Calvanese, D., De Giacomo, G., Rosati, R.: A note on encoding inverse roles and
functional restrictions in ALC knowledge bases. In: DL. pp. 69–71. CEUR (1998)
6. Carral, D., Feier, C., Grau, B.C., Hitzler, P., Horrocks, I.: EL-ifying ontologies. In:
IJCAR (2014), to appear
7. Ding, Y.: Tableau-based reasoning for Description Logics with inverse roles and
number restrictions. Ph.D. thesis, Concordia University, Canada (2008)
8. Ding, Y., Haarslev, V., Wu, J.: A new mapping from ALCI to ALC. In: Calvanese,
D., Franconi, E., Haarslev, V., Lembo, D., Motik, B., Turhan, A., Tessaris, S. (eds.)
DL. CEUR Workshop Proceedings, vol. 250 (2007)
9. Gonçalves, R.S., Matentzoglu, N., Parsia, B., Sattler, U.: The empirical robustness
of Description Logic classification. In: DL. pp. 197–208 (2013)
10. Haarslev, V., Hidde, K., Möller, R., Wessel, M.: The RacerPro knowledge repre-
sentation and reasoning system. Semantic Web J. 3(3), 267–277 (2012)
11. Horrocks, I., Sattler, U.: A tableau decision procedure for SHOIQ. J. of Auto-
mated Reasoning 39(3), 249–276 (2007)
12. Kazakov, Y., Krötzsch, M., Simancik, F.: Concurrent classification of EL ontolo-
gies. In: ISWC. pp. 305–320 (2011)
13. Kontchakov, R., Lutz, C., Toman, D., Wolter, F., Zakharyaschev, M.: The com-
bined approach to ontology-based data access. In: IJCAI. pp. 2656–2661 (2011)
14. Lutz, C., Piro, R., Wolter, F.: Description Logic TBoxes: Model-theoretic charac-
terizations and rewritability. In: IJCAI. pp. 983–988 (2011)
15. Motik, B., Cuenca Grau, B., Horrocks, I., Wu, Z., Fokoue, A., Lutz, C. (eds.):
OWL 2 Web Ontology Language: Profiles. W3C Recommendation (27 October
2009), available at http://www.w3.org/TR/owl2-profiles/
16. Motik, B., Shearer, R., Horrocks, I.: Hypertableau reasoning for Description Logics.
J. Artificial Intelligence Research (JAIR) 36(1), 165–228 (2009)
17. Motik, B., Horrocks, I.: Individual reuse in Description Logic reasoning. In: IJCAR.
pp. 242–258 (2008)
18. Motik, B., Nenov, Y., Piro, R., Horrocks, I., Olteanu, D.: Parallel materialisation
of Datalog programs in centralised, main-memory RDF systems. In: AAAI (2014)
19. Ren, Y., Pan, J.Z., Zhao, Y.: Soundness preserving approximation for TBox rea-
soning. In: AAAI (2010)
20. Sirin, E., Parsia, B., Cuenca Grau, B., Kalyanpur, A., Katz, Y.: Pellet: A practical
OWL-DL reasoner. J. Web Semantics (JWS) 5(2), 51–53 (2007)
21. Song, W., Spencer, B., Du, W.: A transformation approach for classifying
ALCHI(D) ontologies with a consequence-based ALCH reasoner. In: ORE. CEUR,
vol. 1015, pp. 39–45 (2013)
22. Stefanoni, G., Motik, B., Horrocks, I.: Introducing nominals to the combined query
answering approaches for EL. In: AAAI (2013)
23. Tsarkov, D., Horrocks, I.: FaCT++ Description Logic reasoner: System descrip-
tion. 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-defined
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)