Advancing ELK: Not Only Performance Matters

Abstract

This paper reports on the recent development of ELK, a consequence+ ontologies. It covers novel reasoning techniques which based reasoner for E L? aim at improving efficiency and providing foundation for new reasoning services. On the former front we present a simple optimization for handling of role composition 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 without making rules dependent on derived conclusions. This improvement is not visible to the end user but considerably simplifies implementation for incremental reasoning and proof generation. We also present a rewriting of low-level inferences 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 (visual) ontology debugging. We demonstrate the latter capability using a new ELK Protégé plugin.

Introduction

ELK is an ontology reasoner designed for top classification performance on OWL EL ontologies [ 1 ]. Its characteristic features are consequence-based calculus, highly parallelizable 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 E L 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 classification procedure, in particular, the non-deterministic saturation, can complicate the development or weaken the guarantees of such extra services. For example, the composition/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 particular, 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 ]. E E 2 E0 C v C E> C v >

C v D v C v E : D v E 2 O E

9 + reasoning. Most theWe first describe ELK’s consequence-based procedure for E L? 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.

+ is defined using a vocabulary consisting of countably infinite sets The syntax of E L? + concepts are defined using the grammar of (atomic) roles and atomic concepts. E L? C ::= A j > j ? j C1 u C2 j 9R:C, where A is an atomic concept, R a role, and C(i) 2 C. E L+? role chains are defined using the grammar P ::= j R , where is the empty role chain, R a role and 2 P. We usually write role chains as R1 R2 Rn instead of R1 (R2 (Rn )). An E L+? axiom is either a concept inclusion C1 v C2 for C1; C2 2 C or a role inclusion v R for 2 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 E L+? ontology O is a finite set of E L? + is defined in the usual way ( is interpreted as + axioms. Semantics of E L? identity). A concept C is subsumed by D w.r.t. O if O j= 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

+ ontologies is usually performed by applying rules that derive Classification of E L? +-rules that are similar to those logical consequences of axioms. Figure 1 lists the E L? 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 2 O.

+ ontology O = fA v 9R:B, B v 9S:C, R S H v V , Example 1. Consider the E L? v Hg. Then it is possible to derive A v 9V:C using the rules in Figure 1 as follows: A v A Formally, a derivation for E L ontology O (using the rules in Figure 1) is a sequence of E L+? axioms d = f i j i 1g such that each i with i 0 is obtained from axioms f j j 1 j < ig using one of the rules in Figure 1 and axioms in O as side conditions. The size jjdjj 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 = fRj 1 v Rj j 1 j mg [ fCi 1 v 9R0:Ci; 9Rm:Di v Di 1 j 1 i ng [ fCn v Dng. Then one can only derive C0 v D0 by the rules in Figure 1 by deriving quadratically-many intermediate axioms Ci 1 v 9Rj :Ci by E using Rj 1 v Rj 2 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 E L+?. First, we can derive role chains on the right-hand side of role inclusions: 1 v 2 (I j= 1 v 2 if 1I 2I ). Second, we allow role chains to occur in existential restrictions: 9(R ):C is rewritten to 9R:C if = , or to 9R:9 :C otherwise (whenever we write 9 :C we assume that 6= ). The + axioms can be used in derivations, but not in the ontology O. extended E L? Example 2. Below is the derivation for A v 9V:C for the ontology O in Example 1 using the rules in Figure 2:

A v A Rv C0 C v C C> C v > C C v CC vv DE : D v E 2 O Rr C? C9 C9 C 1 v R v 2

1 v R 2 C v 9 :D

C v ? C v D v R

C v 9R:D C v 9 :D v R

C v 9R:E C v 9 1:D

D v ?

D v E 1 v R D v 9 2:E C v 9(R ):E 2 v

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 E L+ axioms such as A v 9(R S H):C and S v S H, the last of which is not even expressible in E L+. 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): + ontology, d a derivation by the rules in Figure 2 for O, Theorem 1. Let O be an E L? and F v G 2 d an (ordinary) E L+? axiom. Then one can construct a derivation e by the rules in Figure 1 for O with F v G 2 e such that jjejj = O(jjdjj2).

The proof of Theorem 1 can be found in the technical report [ 11 ], which also contains 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 + axioms. It is easy to see that the rules in Figby these rules, we mean extended E L? 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 E L? + concept inclusion such + ontology and F v G an E L? that O j= F v G. Then there exists a derivation d using the rules in Figure 2 such that either F v G 2 d or F v ? 2 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 Cu+, C9 or C9 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 Cu in which the premise is composed, by rule C9 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 = fA v 9R:B; B v C; C v Dg. Then the following derivation using the rules in Figure 2 is possible: (+) (+)

A v A In this derivation, axioms (27) and (30) (labeled with +) are composed because they were obtained by rule C9. Hence the inference that has produced (30) is redundant because it is made by an application of C9 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 C9 to a non-composed premise (22): (+)

A v 9R:D by C9(A v 9R: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 Cu to premises derived by Cu+ or apply C9 and C to premises derived by C9 [ 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 9 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 j= 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 j= 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 9 :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 9 :C1 (rules C9 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 9 1:D is already derived. We call this optimization goal-directed rule application.

Example 4. Consider the ontology O = fA v 9R:B; A v 9R:C; B v C; C v Bg. Suppose we want to check whether O j= A v B. Then the following goal-directed non-redundant rule applications can be performed: (+) (+)

A v A 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 9R:C is composed (and thus, e.g., cannot be used in rule C9 like axiom A v 9R:B). Since no further rules need to be applied and the axiom A v B is not derived, we can conclude that O 6j= A v B. Note that if we swap (33) with (38), then the axiom A v 9R: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).

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 E L? [ 13 ]. To illustrate the problem addressed, consider the following example. Example 5. Consider the ontology O = fA v 9L:B; B v 9P:C; C v 9P:D; L P v L; P P v P g. 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 j= 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 9(L P ):C A v 9(L P ):D B v 9(P P ):D A v 9(L P ):D by C (A v 9L:B, L v L, B v 9P:C, P v P ), by C (A v 9(L P ):C, L P v L, C v 9P:D, P v P ), by C (B v 9P:C, P v P , C v 9P:D, P v P ), by C (A v 9L:B, L v L, B v 9(P P ):D, P P v P ).

Now suppose that we also have S v S, S T v R and C v 9(R ):F can be derived as follows: v in the derivation. Then C v 9(S T ):E C v 9(R ):F by C (C v 9S:D, S v S, D v 9 :E,

v T ), by C (C v 9(S T ):E, S T v R, E v 9 :F , v ).

Note that when we replace the rule application (43) with the two rule applications (45) and (46), the third premises D v 9 :E and E v 9 :F used in these applications appear in the derivation before the third premise D v 9(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 Note that the axiom A v 9(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 9(R ):F by C (C v 9S:D, S v R, D v 9(T ):F , (T ) v ).

(43) Let us try to determine when the same conclusion can be derived differently. Suppose that 6= . Then D v 9(T ):F can be only derived by C :

D v 9(T ):F by C (D v 9 :E, v T , E v 9 :F , v ).

(39) (40) (41) (42) (44) (45) (46) 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 2 O would be applied for A v 9L:B and B v 9P:C (derived by Ev), but would not be applied for A v 9L:B and B v 9P:D if B v 9P:D is derived by E from B v 9P:C and C v 9P:D using P P v P 2 O. The reason is that the same conclusion A v 9L:D can be derived in a left-linear way from A v 9L:C (derived by E using L P v L 2 O) and C v 9P: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 goaldirected 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 extending 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 incorrect 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 R9 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.

C+ C v D : A

C v A For example, axiom A v 9R:C in Example 4 was derived by both rules C9 and Cv. We would then not apply C9 to the first conclusion of a ‘composition’ inference by C9, 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 = fA v B u 9R:A; C 9R:Bg. Recall, that concept equivalence C 9R:B represents two axioms C v 9R:B and 9R:B v C. To test O j= A v C, we apply the rules in Figure 2 in a goal-directed way: (+)

A v B A v 9R:A Note that axiom A v 9R:B is derived by rules C9 and Cv, so we would need to consider the second conclusion (51) for applications of C9. Note that the second rule application is a direct result of the equivalence axiom C 9R:B, which was used to replace the subsumer 9R:B in (49) with C and back with 9R: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 concept 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+ using 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. (+) 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 optimization 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 E L 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 subrole 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 subsumptions (many subsumptions are derived by several inferences). The difference translates into time savings. The ANATOMY ontology stands out as the case where the optimization 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 deterministic 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 nondeterministic 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.

1Unless specified otherwise, the ontologies can be downloaded from the ELK project page elk.semanticweb.org 2http://www.ihtsdo.org/licensing/ 3http://www.opengalen.org/sources/sources.html

One can see that deterministic saturation without further optimizations is significantly 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 concept 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 reasoning 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. , Simancˇík , F.: The incredible ELK: From polynomial procedures to efficient reasoning with E L 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 integrated 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 . Bioinformatics 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 E L 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 E L 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. , Simancˇík , F.: Unchain my E L reasoner . In Rosati, R., Rudolph , S. , Zakharyaschev , M., eds. : Proc. 24th Int. Workshop on Description Logics (DL'11) . Volume 745 of CEUR Workshop Proceedings., CEUR-WS.org ( 2011 ) 202 - 212

14. Baader , F. , Lutz , C. , Suntisrivaraporn , B. : Efficient reasoning in E L+ . 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