=Paper=
{{Paper
|id=Vol-1350/paper-27
|storemode=property
|title=Advancing
ELK: Not Only Performance Matters
|pdfUrl=https://ceur-ws.org/Vol-1350/paper-27.pdf
|volume=Vol-1350
|dblpUrl=https://dblp.org/rec/conf/dlog/KazakovK15
}}
==Advancing
ELK: Not Only Performance Matters==
https://ceur-ws.org/Vol-1350/paper-27.pdf
Advancing ELK: Not Only Performance Matters
Yevgeny Kazakov and Pavel Klinov
The University of Ulm, Germany
{yevgeny.kazakov, pavel.klinov}@uni-ulm.de
Abstract. This paper reports on the recent development of ELK, a consequence-
based reasoner for EL+ ⊥ ontologies. It covers novel reasoning techniques which
aim at improving efficiency and providing foundation for new reasoning services.
On the former front we present a simple optimization for handling of role com-
position axioms, such as transitivity, which substantially reduces the number of
rule applications. For the latter, we describe a new rule application strategy that
takes advantage of concept definitions to avoid many redundant inferences with-
out making rules dependent on derived conclusions. This improvement is not vis-
ible to the end user but considerably simplifies implementation for incremental
reasoning and proof generation. We also present a rewriting of low-level infer-
ences used by ELK to higher-level proofs that can be defined in the standard DL
syntax, and thus be used for automatic verification of reasoning results or (vi-
sual) ontology debugging. We demonstrate the latter capability using a new ELK
Protégé plugin.
1 Introduction
ELK is an ontology reasoner designed for top classification performance on OWL EL
ontologies [1]. Its characteristic features are consequence-based calculus, highly par-
allelizable reasoning, and aggressive optimizations to reduce the number of derived
axioms sufficient for classification (deriving all subsumptions between concept names).
Sheer performance has been the sole goal for the first few versions of ELK and
it enabled it to become the reasoner of choice in biomedical circles where large EL
ontologies are built to manage scientific terminologies [2–7]. After that ELK started
to evolve towards providing additional reasoning-related services, such as incremental
classification [8] and proof tracing [9]. It turned out that some traits of ELK’s classi-
fication procedure, in particular, the non-deterministic saturation, can complicate the
development or weaken the guarantees of such extra services. For example, the compo-
sition/decomposition optimization (cf. [1]) has to be off when incrementally retracting
inferences [8]. Also, the proof tracing method guarantees only that all proofs performed
by ELK will be generated, not all proofs supported by the calculus [9]. This, in partic-
ular, means that one cannot in general obtain all justifications [10] from proofs.
In this paper we describe the steps towards adapting the main reasoning procedure
to rectify this sort of issues without major performance setbacks. On the performance
front we show a technique to reduce the number of inferences on roles. We also present
a rewriting of the low-level traced inferences into higher-level proof-based explanations
which could be shown to the user or verified using automated reasoning tools. Due to
the space constraints, some results are deferred to the technical report [11].
C v D1 C v D2
E0 E+
u
CvC C v D1 u D2
E> C v ∃R.D D v ⊥
Cv> E⊥
Cv⊥
CvD
Ev : D v E ∈ O E C v ∃R.D D v E
CvE ∃
C v ∃R.E
C v D1 u D2
E−
u Ci−1 v ∃Ri .Ci (1 ≤ i ≤ k, k ≥ 0)
C v D1 C v D2 E◦ : R1 · · · Rk v R ∈ O
C0 v ∃R.Ck
Fig. 1. Basic inference rules for reasoning in EL+
⊥
2 Consequence-Based Reasoning in EL+
⊥
We first describe ELK’s consequence-based procedure for EL+ ⊥ reasoning. Most the-
oretical results, such as completeness, redundancy elimination, and goal-directed rule
application, are minor variations of [1] but the rules for dealing with role chain axioms
without binarization and rules for reasoning with reflexive roles are new.
2.1 The Description Logic EL+
⊥
The syntax of EL+ ⊥ is defined using a vocabulary consisting of countably infinite sets
of (atomic) roles and atomic concepts. EL+ ⊥ concepts are defined using the grammar
C ::= A | > | ⊥ | C1 u C2 | ∃R.C, where A is an atomic concept, R a role, and
C(i) ∈ C. EL+ ⊥ role chains are defined using the grammar P ::= | R·ρ, where is
the empty role chain, R a role and ρ ∈ P. We usually write role chains as R1 ·R2 · · · Rn
instead of R1 ·(R2 · · · (Rn ·)). An EL+⊥ axiom is either a concept inclusion C1 v C2
for C1 , C2 ∈ C or a role inclusion ρ v R for ρ ∈ P and a role R. We regard the
concept equivalence C1 ≡ C2 as an abbreviation for two concept inclusions C1 v C2
and C2 v C1 . We also call v R a role reflexivity axiom. An EL+ ⊥ ontology O is a finite
set of EL+ ⊥ axioms. Semantics of EL +
⊥ is defined in the usual way ( is interpreted as
identity). A concept C is subsumed by D w.r.t. O if O |= C v D. In this case, we call
C v D an entailed subsumption (w.r.t. O). The ontology classification task requires to
compute all entailed subsumptions between atomic concepts occurring in O.
2.2 Inference Rules
Classification of EL+ ⊥ ontologies is usually performed by applying rules that derive
logical consequences of axioms. Figure 1 lists the EL+ ⊥ -rules that are similar to those
usually considered in the literature [12, 13]. The premises of the rules are written above
the horizontal line, the conclusions below, and the axioms in the ontology (a.k.a. side
conditions) that trigger rule applications after the colon. Note that rule E◦ can be used
with k = 0, in which case it has no premises and uses the reflexivity axiom v R ∈ O.
Example 1. Consider the EL+ ⊥ ontology O = {A v ∃R.B, B v ∃S.C, R·S·H v V ,
v H}. Then it is possible to derive A v ∃V.C using the rules in Figure 1 as follows:
AvA by E0 (), (1)
A v ∃R.B by Ev (A v A) : A v ∃R.B ∈ O, (2)
BvB by E0 (), (3)
B v ∃S.C by Ev (B v B) : B v ∃S.C ∈ O, (4)
C v ∃H.C by E◦ () : v H ∈ O, (5)
A v ∃V.C by E◦ (A v ∃R.B, B v ∃S.C, C v ∃H.C) : R·S·H v V ∈ O. (6)
Formally, a derivation for EL ontology O (using the rules in Figure 1) is a sequence
of EL+ ⊥ axioms d = {αi | i ≥ 1} such that each αi with i ≥ 0 is obtained from axioms
{αj | 1 ≤ j < i} using one of the rules in Figure 1 and axioms in O as side conditions.
The size ||d|| of d is the number of axioms in d. For example, the sequence of axioms
(1)–(6) in Example 1 forms a derivation, in which every axiom is obtained from the
previous axioms by the rules in Figure 1 as indicated next to the axioms.
The rules in Figure 1 are simple to understand but not very efficient to implement.
The problem is caused by rule E◦ , which may produce many conclusions for ontologies
with deep role hierarchies. For example, consider O = {Rj−1 v Rj | 1 ≤ j ≤ m} ∪
{Ci−1 v ∃R0 .Ci , ∃Rm .Di v Di−1 | 1 ≤ i ≤ n} ∪ {Cn v Dn }. Then one can only
derive C0 v D0 by the rules in Figure 1 by deriving quadratically-many intermediate
axioms Ci−1 v ∃Rj .Ci by E◦ using Rj−1 v Rj ∈ O (1 ≤ i ≤ n, 1 ≤ j ≤ m).
Therefore, ELK implements optimized rules listed in Figure 2 that help avoiding this
problem by deriving subsumptions on role (chains) separately [1]. To formulate these
rules, we have slightly extended the syntax of EL+ ⊥ . First, we can derive role chains on
the right-hand side of role inclusions: ρ1 v ρ2 (I |= ρ1 v ρ2 if ρI1 ⊆ ρI2 ). Second, we
allow role chains to occur in existential restrictions: ∃(R·ρ).C is rewritten to ∃R.C if
ρ = , or to ∃R.∃ρ.C otherwise (whenever we write ∃ρ.C we assume that ρ 6= ). The
extended EL+ ⊥ axioms can be used in derivations, but not in the ontology O.
Example 2. Below is the derivation for A v ∃V.C for the ontology O in Example 1
using the rules in Figure 2:
AvA by C0 (), (7)
A v ∃R.B by Cv (A v A) : A v ∃R.B ∈ O, (8)
RvR by R0 (), (9)
BvB by C0 (), (10)
B v ∃S.C by Cv (B v B) : B v ∃S.C ∈ O, (11)
SvS by R0 (), (12)
CvC by C0 (), (13)
v by R0 (), (14)
vH by Rv ( v ) : v H ∈ O, (15)
S v S·H by Rr (S v S, v H), (16)
A v ∃(R·S·H).C by C◦ (A v ∃R.B, R v R, B v ∃S.C, S v S·H), (17)
v R ρ 1 v ρ2
R0 Rl
ρvρ ρ1 v R·ρ2
ρ1 v ρ2 ρ 1 v R v ρ2
Rv : ρ2 v R ∈ O Rr
ρ1 v R ρ1 v R·ρ2
C v ∃ρ.D D v ⊥
C0 C⊥
CvC Cv⊥
CvD vR
C> C∃
Cv> C v ∃R.D
CvD C v ∃ρ.D ρ v R D v E
Cv :DvE∈O C∃
CvE C v ∃R.E
C v D1 u D2 C v ∃ρ1 .D ρ1 v R D v ∃ρ2 .E ρ2 v ρ
C−
u C◦
C v D1 C v D2 C v ∃(R·ρ).E
C v D1 C v D2
C+
u
C v D1 u D2
Fig. 2. Optimized inference rules for reasoning in EL+
⊥ implemented in ELK
R·S·H v R·S·H by R0 (), (18)
R·S·H v V by Rv (R·S·H v R·S·H) : R·S·H v V ∈ O, (19)
A v ∃V.C by C∃ (A v ∃(R·S·H).C, R·S·H v V, C v C). (20)
As can be seen from Examples 1 and 2, derivations using the rules in Figure 2 can
be more difficult to understand because they use relatively complex rules such as Rr
and C◦ and manipulate with extended EL+ axioms such as A v ∃(R·S·H).C and
S v S·H, the last of which is not even expressible in EL+ . Fortunately, it is always
possible to rewrite any derivation by the rules in Figure 2 into the one by the rules in
Figure 1 using a simple recursive procedure (with an unavoidable quadratic blowup):
Theorem 1. Let O be an EL+ ⊥ ontology, d a derivation by the rules in Figure 2 for O,
and F v G ∈ d an (ordinary) EL+ ⊥ axiom. Then one can construct a derivation e by
the rules in Figure 1 for O with F v G ∈ e such that ||e|| = O(||d||2 ).
The proof of Theorem 1 can be found in the technical report [11], which also con-
tains an overview of the Protégé plug-in for displaying proofs based on this result.
2.3 Composed Conclusions, Redundancy and Completeness
From now on, we focus in the rules in Figure 2, so when we talk about axioms derived
by these rules, we mean extended EL+ ⊥ axioms. It is easy to see that the rules in Fig-
ure 2 are sound, that is, the conclusions of the rules are logical consequences of the
premises and the side conditions, if there are any. Therefore, every derivation contains
only axioms entailed by the ontology. It turns out that the converse property also holds:
Theorem 2. Let O be an EL+ +
⊥ ontology and F v G an EL⊥ concept inclusion such
that O |= F v G. Then there exists a derivation d using the rules in Figure 2 such that
either F v G ∈ d or F v ⊥ ∈ d.
Similarly to existing results [12, 1], Theorem 2 is proved by constructing a canonical
model using the set of all derivable axioms. One can actually prove a stronger version
of this theorem, namely that every entailed subsumption is derivable by an optimized
derivation—a derivation which does not use a certain kind of redundant inferences [11].
Definition 1. We say that an axiom α in a derivation d is composed if can be obtained
by rules C+
u , C∃ or C∃ from the previous axioms. An application of a rule in Figure 2
to premises in d is redundant if it is an application by rule C−
u in which the premise is
composed, by rule C∃ in which the first premise is composed, or by rule C◦ in which
the first or the third premise is composed. The derivation d is optimized if every axiom
α in d is obtained from the previous axioms using a non-redundant rule application.
Example 3. Consider the ontology O = {A v ∃R.B, B v C, C v D}. Then the fol-
lowing derivation using the rules in Figure 2 is possible:
AvA by C0 (), (21)
A v ∃R.B by Cv (A v A) : A v ∃R.B ∈ O, (22)
BvB by C0 (), (23)
BvC by Cv (B v B) : B v C ∈ O, (24)
BvD by Cv (B v C) : C v D ∈ O, (25)
RvR by R0 (), (26)
(+) A v ∃R.C by C∃ (A v ∃R.B, R v R, B v C), (27)
CvC by C0 (), (28)
CvD by Cv (C v C) : C v D ∈ O, (29)
(+) A v ∃R.D by C∃ (A v ∃R.C, R v R, C v D). (30)
In this derivation, axioms (27) and (30) (labeled with +) are composed because they
were obtained by rule C∃ . Hence the inference that has produced (30) is redundant
because it is made by an application of C∃ to a composed first premise (27). Still,
the derivation (21)–(30) is optimized because (30) can be obtained from the previous
axioms by another (non-redundant) application of C∃ to a non-composed premise (22):
(+) A v ∃R.D by C∃ (A v ∃R.B, R v R, B v D). (31)
In other words, since a derivation is a sequence of axioms and not a sequence of rule
applications, it matters by which inferences axioms can be obtained from the previous
axioms. Note that if (25) is removed from the derivation, then the inference (31) is no
longer possible and the derivation becomes non-optimized.
In practice, the optimization above means that when applying the rules in Figure 2
to check entailment of concept inclusion, it is not necessary to apply C−
u to premises
derived by C+ u or apply C∃ and C◦ to premises derived by C∃ [1].
2.4 The Subformula Property and Goal-Directed Rule Application
So far Theorem 2 cannot be used for effectively checking if a given subsumption C v
D is entailed by the ontology O since there are infinitely many axioms that can be
derived by the rules in Figure 2—already C0 can produce infinitely many conclusions.
It turns out, it is sufficient to derive only axioms of the form ρ1 v ρ2 , C1 v C2 , and
C1 v ∃ρ2 .C2 such that all concepts Ci and role chains ρi (i = 1, 2) occur (possibly as
sub-expressions) either in the ontology O or in the given subsumption F v G tested for
entailment [1]. In other words, if O |= F v G then F v G or F v ⊥ is derivable by the
rules in Figure 2 without creating new concepts or role chains. We refer to this property
as subformula property. The subformula property implies that checking entailment O |=
F v G can be done in polynomial time since there are at most polynomially-many
different axioms of the above forms, and one can compute a derivation d containing all
such axioms by repeatedly applying the rules in Figure 2.
The rules, however, can be restricted even further. Specifically, an axiom C1 v C2
needs to be derived in d only if C1 = F for the tested subsumption F v G or if some
non-composed axiom of the form C v ∃ρ.C1 is already derived in d. Indeed, it is easy
to observe from the rules in Figure 2 that an axiom C1 v C2 can be used in a rule
application only if this rule derives a concept inclusion axiom with the same left-hand
side C1 or it uses another non-composed axiom of the form C v ∃ρ.C1 (rules C∃
and C◦ ). Similarly, an axiom ρ1 v ρ2 needs to be derived only if ρ1 = or if some
other non-composed axiom of the form C v ∃ρ1 .D is already derived. We call this
optimization goal-directed rule application.
Example 4. Consider the ontology O = {A v ∃R.B, A v ∃R.C, B v C, C v B}.
Suppose we want to check whether O |= A v B. Then the following goal-directed
non-redundant rule applications can be performed:
AvA by C0 (), (32)
A v ∃R.B by Cv (A v A) : A v ∃R.B ∈ O, (33)
BvB by R0 (), (34)
BvC by Rv (B v B) : B v C ∈ O, (35)
RvR by R0 (), (36)
(+) A v ∃R.C by C∃ (A v ∃R.B, R v R, B v C), (37)
(+) A v ∃R.C by Cv (A v A) : A v ∃R.C ∈ O. (38)
Note that deriving axioms with the left-hand side C (e.g., C v C by rule C0 ) is not
necessary since the axiom A v ∃R.C is composed (and thus, e.g., cannot be used in
rule C∃ like axiom A v ∃R.B). Since no further rules need to be applied and the axiom
A v B is not derived, we can conclude that O 6|= A v B. Note that if we swap (33)
with (38), then the axiom A v ∃R.C would not be composed and we would need to
derive subsumptions C v C and C v B by rules C0 and Cv . Thus the set of derived
axioms depends on the order in which the rules are applied.
Note that if a derivation d contains C v D or ρ1 v ρ2 then C v C or ρ1 v ρ1 must
be derived in d respectively by C0 and R0 before that. Therefore, to save space, from
now on we skip applications of the rules C0 and R0 (e.g., like (32), (34), and (36) in
Example 4). We will also skip application of the rules Cv and Rv producing axioms in
the ontology from the conclusions of C0 and R0 (e.g., like (33) and (35) in Example 4).
3 Avoiding Duplicate Role Compositions
In this section, we present an optimization, using which one can avoid some duplicate
conclusions of rule C◦ . Intuitively, this optimization is designed to deal more efficiently
with specific role chain axioms such as transitivity T ·T v T . It is closely related to a
similar optimization for role chain axioms presented previously for a fragment of EL+ ⊥
[13]. To illustrate the problem addressed, consider the following example.
Example 5. Consider the ontology O = {A v ∃L.B, B v ∃P.C, C v ∃P.D, L·P v
L, P ·P v P }. The roles L and P can be thought of as expressing the ‘located-in’ and
‘part-of’ relations. So the last axiom of O, in particular, expresses that if x is located
in y and y is a part of z then x is located in z. Let us try to determine whether O |=
A v B using goal-direct application of rules (skipping applications of C0 and R0 , and
applications of Cv , Rv producing axioms in O as noted before):
A v ∃(L·P ).C by C◦ (A v ∃L.B, L v L, B v ∃P.C, P v P ), (39)
A v ∃(L·P ).D by C◦ (A v ∃(L·P ).C, L·P v L, C v ∃P.D, P v P ), (40)
B v ∃(P ·P ).D by C◦ (B v ∃P.C, P v P , C v ∃P.D, P v P ), (41)
A v ∃(L·P ).D by C◦ (A v ∃L.B, L v L, B v ∃(P ·P ).D, P ·P v P ). (42)
Note that the axiom A v ∃(L·P ).D was derived two times by C0 in (40) and (42).
Intuitively, this is because the role chain inclusion L·P ·P v L·P can be proved in two
ways: either as (L·P )·P v L·P using L·P v L or as L·(P ·P ) v L·P using P ·P v P .
In general, suppose that we have a derivation where some axiom is derived by C◦ :
C v ∃(R·ρ).F by C◦ (C v ∃S.D, S v R, D v ∃(T ·µ).F , (T ·µ) v ρ). (43)
Let us try to determine when the same conclusion can be derived differently. Suppose
that µ 6= . Then D v ∃(T ·µ).F can be only derived by C◦ :
D v ∃(T ·µ).F by C◦ (D v ∃τ.E, τ v T , E v ∃η.F , η v µ). (44)
Now suppose that we also have S v S, S·T v R and η v ρ in the derivation. Then
C v ∃(R·ρ).F can be derived as follows:
C v ∃(S·T ).E by C◦ (C v ∃S.D, S v S, D v ∃τ.E, τ v T ), (45)
C v ∃(R·ρ).F by C◦ (C v ∃(S·T ).E, S·T v R, E v ∃η.F , η v ρ). (46)
Note that when we replace the rule application (43) with the two rule applications
(45) and (46), the third premises D v ∃τ.E and E v ∃η.F used in these applications
appear in the derivation before the third premise D v ∃(T ·µ).F of (43) since the
latter was obtained from the former by (44). Therefore, if we apply this transformation
repeatedly to all inferences by C◦ , it will always terminate.
To summarize, we can always avoid applying C◦ with S v R and T ·µ v ρ as
the second and the last premises if µ 6= and we can derive S·T v R (S v S is
always derivable by R0 ) and τ v ρ for every derivable τ v µ. Due to the subformula
property, we can precompute all subsumptions on role chains occurring in the ontology
and compute all pairs hρ1 v R, ρ2 v ρi of such role subsumptions with ρ1 , ρ2 and R·ρ
occurring in the ontology, excluding the pairs hS v R, T ·µ v ρi for which the above
condition holds. Only the remaining pairs of subsumptions should then be used in C◦ .
Example 6. Continuing Example 5, we can show that the above conditions hold for the
pair hS v R, T ·µ v ρi = hL v L, P ·P v P i. Indeed, S·T v R = L·P v L can
be derived, and since µ = ρ = P , τ v ρ is derivable if τ v µ is. Thus, the pair
hL v L, P ·P v P i should not be used in C◦ , and thus inference (42) is not necessary.
One can show that the pair hP v P, P ·P v P i should not be used in C◦ as well.
As mentioned, there is a close relation of the optimization above with a similar
optimization for rules in Figure 1 [13]. The main idea is to identify the role chain axioms
ρ v R for which rule E◦ can be applied in a left-linear way, that is, only if all premises
starting from the second one are derived by rules other than E◦ with k ≥ 2. This is the
case, e.g., for both axioms L·P v L and P ·P v P from ontology O in Example 5.
For example, rule E◦ using L·P v L ∈ O would be applied for A v ∃L.B and
B v ∃P.C (derived by Ev ), but would not be applied for A v ∃L.B and B v ∃P.D
if B v ∃P.D is derived by E◦ from B v ∃P.C and C v ∃P.D using P ·P v P ∈ O.
The reason is that the same conclusion A v ∃L.D can be derived in a left-linear way
from A v ∃L.C (derived by E◦ using L·P v L ∈ O) and C v ∃P.D (derived by Ev ).
The main difference between the two optimizations, is that, due to the differences in the
rules in Figure 1 and Figure 2, instead of classifying which stated role chain axioms
can be used in a left-linear way, we determine which derived role chain axioms should
be ‘concatenated’ in rule C◦ . The latter is algorithmically easier to determine using the
condition formulated above.
4 Deterministic Saturation
Recall from Example 4 that the set of axioms obtained by applying the rules in a goal-
directed way may depend on the order in which the rules are applied. Although this
side effect has no impact on reasoning results, it introduces some difficulties when ex-
tending ELK reasoning services beyond checking of logical entailment. Specifically,
the procedures for incremental reasoning [8] and proof generation [9] implemented in
ELK, require repeating some rule applications performed in the derivation, and if the
rules are applied in a different order than originally, the procedures may result in incor-
rect results. In this section we describe a modification of our rule application procedure
for which the derived axioms do not depend on the order of rule application.
Recall from Section 2.3 that to determine whether a rule such as R∃ should be
applied to some axioms in the derivation, i.e., it is not redundant, one has to check which
of these axioms are composed, i.e., can be derived by certain rules from the previous
axioms in the derivation. This property ensures that only necessary rules are applied, but
it can make rule application dependent on when (i.e, after which axioms) the premises
were derived. Instead, we may slightly relax this requirement and decide whether an
axiom is composed or not only based on the rules by which it was actually derived,
which would make rule applications not to depend on other axioms in the derivation.
CvA CvD
C−
≡ :A≡D∈O C+
≡ :A≡D∈O
CvD CvA
Fig. 3. The new inference rules for concept definitions
For example, axiom A v ∃R.C in Example 4 was derived by both rules C∃ and Cv .
We would then not apply C∃ to the first conclusion of a ‘composition’ inference by C∃ ,
but apply it to the second conclusion of ‘non-composition’ inference by Cv . Clearly,
the advantage here is that it does not matter which of the two inferences was made
first. It may seem that axioms are rarely derived by multiple rules, so the relaxed rule
application strategy might not result in too many unnecessary inferences. The following
example illustrates that this may not be really the case in practice.
Example 7. Consider the ontology O = {A v B u ∃R.A, C ≡ ∃R.B}. Recall, that
concept equivalence C ≡ ∃R.B represents two axioms C v ∃R.B and ∃R.B v C. To
test O |= A v C, we apply the rules in Figure 2 in a goal-directed way:
AvB by C−
u (A v B u ∃R.A), (47)
A v ∃R.A by C−
u (A v B u ∃R.A), (48)
(+) A v ∃R.B by C∃ (A v ∃R.A, R v R, A v B), (49)
AvC by Cv (A v ∃R.B) : ∃R.B v C ∈ O, (50)
A v ∃R.B by Cv (A v C) : C v ∃R.B. (51)
Note that axiom A v ∃R.B is derived by rules C∃ and Cv , so we would need to
consider the second conclusion (51) for applications of C∃ . Note that the second rule
application is a direct result of the equivalence axiom C ≡ ∃R.B, which was used to
replace the subsumer ∃R.B in (49) with C and back with ∃R.B. So it is actually not
possible to have application (51) before (49).
The scenario illustrated in Example 7 is rather common: whenever an axiom C v D
is derived and D occurs in some concept equivalence in the ontology, the same axiom
C v D will be derived again. To avoid such duplicate inferences, we introduce new
rules in Figure 3 to deal specifically with concept definitions—concept equivalences
A ≡ D where A is a (defined) atomic concept. Most concept equivalences in existing
ontologies are of this form. We assume that all concept equivalences in O are concept
definitions and each atomic concept A is defined in at most one of them; remaining con-
cept equivalences can be always replaced with concept inclusions. Finally, we extend
Definition 1 by allowing composed axioms to be obtained by rule C+ ≡ and redundant
rule applications to include applications by rule C−≡ in which the premise is composed.
Note that if the premise of C− ≡ is composed, then it can only be obtained by C+
≡ us-
ing the same concept definition A ≡ D, and hence the conclusion of this rule must be
already derived.
Example 8. Continuing Example 7, with the new rules in Figure 3 we will have just rule
application (52) instead of (50)–(51); the application of rule C−
≡ to (52) is redundant.
(+) A v C by C+
≡ (A v ∃R.B) : C ≡ ∃R.B ∈ O. (52)
Table 1. Summary information for the test ontologies (numbers of the different kinds of axioms)
Ontology C v D C ≡ D R v S R · R v R R1 · R2 v S
EL-GALEN 25,563 9,968 958 58 0
GALEN7 27,820 15,270 1000 0 385
GALEN8 53,449 113,622 1024 0 385
SNOMED CT (Jan 2014) 229,330 69,908 11 0 1
ANATOMY 17,551 21,831 4 3 2
5 Preliminary Experimental Evaluation
In this section we present the preliminary results of empirical evaluation of the two
new reasoning techniques described in Sections 3 and 4: the role composition opti-
mization and the deterministic saturation using new rules for concept definitions. For
both experiments we use a set of the well-known biomedical ontologies:1 the July 2014
version of SNOMED CT,2 three versions of OpenGALEN3 (EL-GALEN, GALEN7,
and GALEN8), and ANATOMY (an experimental version of SNOMED CT which uses
role chain axioms to model the body structure). These ontologies have been frequently
used in the past for evaluation of EL reasoners [14, 15, 1]. The summary information
about these ontologies is presented in Table 1.
For experiments we used a development version of ELK 0.5. The experimental setup
is the same for all experiments: each ontology is classified 20 times, 10 warm-up runs
to exclude the effects of JIT compilation and 10 measured runs, for which the results
are averaged. The combined loading + classification wall clock time (in ms.) is used as
the main performance metric. We used a PC with Intel Core i5-2520M 2.50GHz CPU,
Java 1.6 and 4GB RAM available to JVM.
The first experiment evaluates effectiveness of the role composition optimization
described in Section 3. All ontologies (except for SNOMED CT in which the only sub-
role chain axiom has no effect) are classified with the optimization being turned on and
off. The results are shown in Table 2. It can be seen that in most cases the optimization
considerably reduces the number of inferences as well the number of derived subsump-
tions (many subsumptions are derived by several inferences). The difference translates
into time savings. The ANATOMY ontology stands out as the case where the optimiza-
tion is critically important since it cuts down the number of inferences by rule C◦ by
nearly an order of magnitude.
The aim of the the second experiment is to evaluate the effectiveness of the deter-
ministic saturation optimization described in Section 4. We compare the classification
time and the number of derived axioms in three cases: a) with the ELK’ current non-
deterministic saturation [1], b) with deterministic saturation using the rules in Figure 2,
and c) with deterministic saturation using the additional rules for concept definitions
(see Figure 3). The results are shown in Table 3.
1
Unless specified otherwise, the ontologies can be downloaded from the ELK project page
elk.semanticweb.org
2
http://www.ihtsdo.org/licensing/
3
http://www.opengalen.org/sources/sources.html
Table 2. Evaluation of the role composition optimization from Section 3
Ontology Classification time Inferences Derived subsumptions
Optimization On Off On Off On Off
EL-GALEN 964 1,039 2,080,194 2,207,823 1,485,247 1,550,695
GALEN7 1,632 1,998 5,707,082 7,001,796 2,787,261 2,952,952
GALEN8 15,587 16,981 40,239,327 49,719,156 19,377,172 20,136,178
ANATOMY 8,957 27,766 45,466,892 176,130,924 7,105,923 10,223,484
Table 3. Evaluation of deterministic saturation (see Section 3). The shortcuts “non-det”, “det”,
and “det+defn” stand for non-deterministic saturation, unoptimized deterministic saturation, de-
terministic saturation with the new optimized rules for handling of concept definitions.
Ontology Classification time Inferences Derived subsumptions
non-det det det+defn non-det det det+defn non-det det det+defn
EL-GALEN 959 1,513 1,032 2.1M 4.2M 2.3M 1.5M 2.7M 1.9M
GALEN7 1,984 3,408 2,699 5.7M 11.6M 9.9M 2.8M 5.3M 4.7M
GALEN8 16,750 27,339 19,866 40.2M 93.7M 65.3M 19.4M 37.2M 28.4M
SNOMED CT 14,441 21,791 15,431 25.5M 54.1M 31.2M 17.1M 30.3M 23.6M
ANATOMY 9,183 15,546 9,875 45.5M 73.0M 47.2M 7.1M 12.1M 8.3M
One can see that deterministic saturation without further optimizations is signifi-
cantly slower and often makes nearly twice as many inferences as non-deterministic
saturation. This is largely because many axioms are derived by multiple inferences due
to equivalence axioms (as illustrated in Example 3). The special rules to deal with con-
cept definitions reduce such redundant derivations and improve performance so that it
is close to that of non-deterministic saturation. Still in some cases, e.g., for GALEN7
and GALEN8, the difference between non-deterministic and optimized deterministic
strategies is visible and it remains our goal to investigate how it can be reduced even
further.
6 Summary
The paper presented several recent developments in ELK which range from novel rea-
soning optimizations, such as efficient handling of role chain axioms, to modifications
aimed at supporting additional reasoning services, such as proof-based explanations.
Our experiments show that the latter changes may result in minor performance setbacks,
and it remains our future goal to investigate how to avoid even such minor performance
compromises.
References
1. Kazakov, Y., Krötzsch, M., Simančík, F.: The incredible ELK: From polynomial procedures
to efficient reasoning with EL ontologies. J. of Automated Reasoning 53(1) (2014) 1–61
2. Harris, M.A., Lock, A., Bühler, J., Oliver, S.G., Wood, V.: FYPO: the fission yeast phenotype
ontology. Bioinformatics 29(13) (2013) 1671–1678
3. Hoehndorf, R., Dumontier, M., Gkoutos, G.V.: Identifying aberrant pathways through inte-
grated analysis of knowledge in pharmacogenomics. Bioinformatics 28(16) (2012) 2169–
2175
4. Hoehndorf, R., Harris, M.A., Herre, H., Rustici, G., Gkoutos, G.V.: Semantic integration of
physiology phenotypes with an application to the cellular phenotype ontology. Bioinformat-
ics 28(13) (2012) 1783–1789
5. Jupp, S., Stevens, R., Hoehndorf, R.: Logical gene ontology annotations (GOAL): exploring
gene ontology annotations with OWL. J. of Biomedical Semantics 3(Suppl 1)(S3) (2012)
1–16
6. Osumi-Sutherland, D., Reeve, S., Mungall, C.J., Neuhaus, F., Ruttenberg, A., Jefferis,
G.S.X.E., Armstrong, J.D.: A strategy for building neuroanatomy ontologies. Bioinformatics
28(9) (2012) 1262–1269
7. The Gene Ontology Consortium: Gene ontology annotations and resources. Nucleic Acids
Res (2012)
8. Kazakov, Y., Klinov, P.: Incremental reasoning in OWL EL without bookkeeping. In: The
Semantic Web - ISWC 2013 - 12th International Semantic Web Conference, Sydney, NSW,
Australia, October 21-25, 2013, Proceedings, Part I. (2013) 232–247
9. Kazakov, Y., Klinov, P.: Goal-directed tracing of inferences in EL ontologies. In: The
Semantic Web - ISWC 2014 - 13th International Semantic Web Conference, Riva del Garda,
Italy, October 19-23, 2014. Proceedings, Part II. (2014) 196–211
10. Kalyanpur, A., Parsia, B., Horridge, M., Sirin, E.: Finding all justifications of OWL DL
entailments. In Aberer, K., Choi, K.S., Noy, N., Allemang, D., Lee, K.I., Nixon, L., Golbeck,
J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber, G., Cudré-Mauroux, P., eds.: Proc. 6th
Int. Semantic Web Conf. (ISWC’07). Volume 4825 of LNCS., Springer (2007) 267–280
11. Kazakov, Y., Klinov, P.: Advancing ELK: Not only perormance matters. Technical report,
University of Ulm (2015) available from http://http://elk.semanticweb.org/
publications/elk-advancing-trdl-2015.pdf.
12. Baader, F., Brandt, S., Lutz, C.: Pushing the EL envelope. In Kaelbling, L., Saffiotti, A., eds.:
Proc. 19th Int. Joint Conf. on Artificial Intelligence (IJCAI’05), Professional Book Center
(2005) 364–369
13. Kazakov, Y., Krötzsch, M., Simančík, F.: Unchain my EL reasoner. In Rosati, R., Rudolph,
S., Zakharyaschev, M., eds.: Proc. 24th Int. Workshop on Description Logics (DL’11). Vol-
ume 745 of CEUR Workshop Proceedings., CEUR-WS.org (2011) 202–212
14. Baader, F., Lutz, C., Suntisrivaraporn, B.: Efficient reasoning in EL+ . In Parsia, B., Sattler,
U., Toman, D., eds.: Proc. 19th Int. Workshop on Description Logics (DL’06). Volume 189
of CEUR Workshop Proceedings., CEUR-WS.org (2006)
15. Lawley, M.J., Bousquet, C.: Fast classification in Protégé: Snorocket as an OWL 2 EL
reasoner. In: Proc. 6th Australasian Ontology Workshop (IAOA’10). (2010) 45–49