Goal-Directed Tracing of Inferences in EL Ontologies

Abstract

EL is a family of tractable Description Logics (DLs) that is the basis of the OWL 2 EL profile. Unlike for many expressive DLs, reasoning in EL can be performed by computing a deductively-closed set of logical consequences of some specific form. In some ontology-based applications, e.g., for ontology debugging, knowing the logical consequences of the ontology axioms is often not sufficient. The user also needs to know from which axioms and how the consequences were derived. Although it is possible to keep track of all inferences applied during reasoning, this is usually not done in practice to avoid the overheads. In this paper, we present a goal-directed method that can generate inferences for selected consequences in the deductive closure without re-applying all rules from scratch. We provide an empirical evaluation demonstrating that the method is fast and economical for large EL ontologies. Although the main benefits are demonstrated for EL reasoning, the method can be easily extended to other procedures based on deductive closure computation using fixed sets of rules.

-

The majority of existing DL reasoners are based on optimized (hyper)tableau-based procedures which essentially work by trying to construct counter-models for the entailment [ 19, 15, 20 ]. If the reasoner could not find a counter-model by trying all alternatives, it declares that the entailment holds. It is not easy to use such procedures to generate an explanation for the entailment, or even to determine which axioms are responsible for the entailment, because the axioms that were used to construct the models are not necessarily the ones that are causing the clash. Recently another kind of reasoning procedures, which work by deriving logical consequences of ontology axioms directly, became popular. Such consequence-based procedures were first introduced for the E L family of tractable ontology languages [ 1 ], and later the same principle has been extended to more expressive (non-tractable) languages such as Horn-SHIQ and ALCH [ 9, 18 ]. The consequence-based procedures work by computing the closure under the rules by forward chaining. The inference rules make sure that the result is complete—all entailed conclusions of interest can be simply read off of the closure.

It is easy to extend any consequence-based procedure so that for each derived conclusion, it also records the inferences that have produced it. This way, one can easily generate proofs for the entailed conclusions. Unfortunately, saving all applied inferences during reasoning is not practical, as each conclusion could be derived in many ways and storing all inferences requires a lot of memory. In practice, one usually does not need to retrieve all inferences, but just inferences for some particular (e.g., unexpected) consequences. In this paper, we demonstrate how these inferences can be traced in a goal-directed way using the pre-computed set of conclusions. The main idea, is to split the conclusions on small partitions, so that most inferences are applied within each individual partition. It is then possible to re-compute the inferences for conclusions within each partition by forward chaining using conclusions from other partitions as set of support. A similar idea has been recently used for incremental reasoning in E L+ [ 10 ]. We demonstrate empirically that only a small fraction of inferences is produced when generating proofs for E L+ consequences and that the inferences can be computed in just a few milliseconds even for ontologies with hundreds thousands of axioms. Some omitted details, e.g., proofs, can be found in the technical report [ 11 ]. 2

Related Work

In the context of ontologies, most research relevant to the issue of explanations has revolved around justifications—the minimal subsets of the ontology which entail the result [ 5, 8, 3, 7, 16 ]. For simple ontologies, justifications are often small and can be computed using generic axiom pinpointing procedures, e.g. based on model-based diagnosis [ 17 ], that use the decision procedure for the target (monotonic) logic as a blackbox. While these procedures can significantly narrow down the set of relevant axioms, it is still up to the user to understand how to obtain the result from the justifications.

The fact that justifications are minimal subsets is useful to the user but also makes them intractable to compute [ 16 ]. Much research has gone into developing optimizations to cope with this complexity in practical cases. For example, employing ontology modularity techniques for black-box methods can be seen as a step towards goaldirected behavior [ 5 ]. The so-called locality-based modules [ 6 ] are well-defined fragments of the ontology which, first, can be computed fast using syntactic analysis and, second, contain all justifications for a given entailment. Modules bound the search for justification to an (often small) set of axioms. Using our goal-directed tracing procedure, one can limit the sets of relevant axioms even further: it is sufficient to take all axioms used in side conditions of the computed inferences to obtain all axioms that could be used in proofs. On the other hand, the glass-box methods (e.g., [ 3, 4 ]) tackle the problem by using the properties of the underlying reasoning procedure (instead of using it as a black-box). They are, however, not goal-directed and work similarly to what we below call ‘full tracing’. Our method, in contrast, exploits specific properties of the inference system also to perform computations in a goal-directed way. 3 3.1

Preliminaries

The Description Logic EL+

The syntax of E L+ is defined using a vocabulary consisting of countably infinite sets of (atomic) roles and atomic concepts. E L+ concepts are defined using the grammar C ::= A j > j C1 u C2+j a9xRio:mC,iswehiethreerAa cisonanceapttoimnciclucsoionnceCp1t, vR Can2 afotormCi1c; rCol2e,2anCd, C; C1; C2 2 C. An E L a role inclusion R v S, or a role composition R1 role names. An E L+ ontology O is a finite set of E LR+2 vaxiSo,mws.hEernetaRil;mRen1t; oRf2a;xSioamres by an ontology is defined in a usual way; a formal definition can be found in [ 11 ]. 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.

3.2 Inferences, Inference Rules, and Proofs

Let Exp be a fixed countable set of expressions. An inference over Exp is an object inf which is assigned with a finite set of premises inf:Premises Exp and a conclusion inf:conclusion 2 Exp.1 When inf:Premises = ;, we say that inf is an initialization inference. An inference rule R over Exp is a countable set of inferences over Exp; it is an initialization rule if all these inferences are initialization inferences. In this paper, we view an inference system as one inference rule R representing all of their inferences.

We say that a set of expressions Exp Exp is closed under an inference inf if inf:Premises Exp implies inf:conclusion 2 Exp. Exp is closed under an inference rule R if Exp is closed under every inference inf 2 R. The closure under R is the smallest set of expressions Closure(R) that is closed under R. Note that Closure(R) is always empty if R does not contain initialization inferences.

We will often restrict inference rules to subsets of premises. Let Exp Exp be a set of expressions, and R an inference rule. By R(Exp) (R[Exp], RhExpi) we denote the rule consisting of all inferences inf 2 R such that inf:Premises Exp (respectively Exp inf:Premises, and inf:conclusion 2 Exp). We can arbitrarily combine these filters: for example, R[Exp1](Exp2)hExp3i consists of those inferences in R whose premises contain all expressions from Exp1, are a subset of Exp2, and produce a conclusion in Exp3. The order of filters is not relevant: R[Exp1](Exp2)hExp3i is the same as, e.g, R(Exp2)hExp3i[Exp1]. For simplicity, we write R(), R[], R(exp), R[exp], and Rhexpi instead of R(;), R[;], R(fexpg), R[fexpg], and Rhfexpgi respectively. Note that R[] = RhExpi = R and R() consists of all initialization inferences in R.

A proof (in R) is a sequence of inferences p = inf1; : : : ; infn (infi 2 R, 1 i n) such that infj :Premises finfi:conclusion j 1 i < jg for each j with 1 j n. If exp = infn:conclusion then we say p is a proof for exp. A proof p = inf1; : : : ; infn for exp is minimal if no strict sub-sequence of inf1; : : : ; infn is a proof for exp. Note that in this case infi:conclusion 6= infj :conclusion when i 6= j (1 i; j n). 3.3

The Reasoning Procedure for EL+

The E L+ reasoning procedure works by applying inference rules to derive subsumptions between concepts. In this paper, we use a variant of the rules that does not require normalization of the input ontology [ 13 ]. The rules for E L+ are given in Fig. 1, where the premises (if any) are given above the horizontal line, and the conclusions below. Some rules have side conditions given after the colon that restrict the expressions to which the rules are applicable. For example, rule Ru+ contains one inference inf for each C; D1; D2, such that D1 u D2 occurs in O with inf:Premises = fC v D1; C v D2g, 1There can be different inferences with the same sets of premises and the same conclusion. R0 C v C : C occurs in O R> C v > R R

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

C v D1 u D2 u C v D1 C v D2 : C and > occur in O

R9 R Ru+ C Cv vD1D1Cu vD2D2 : D1 u D2 occurs in O

E v 9R:C C v D : 9S:D occurs in O

E v 9S:D R vO S E v 9R1:C C v 9R2:D

E v 9S:D

S1 S2 v S 2 O : R1 vO S1

R2 vO S2 inf:conclusion = C v D1 u D2. The side conditions of rules R9 and R use the closure vO of role inclusion axioms—the smallest reflexive transitive relation such that R v S 2 O implies R vO S. Note that the axioms in the ontology O are only used in side conditions of the rules and never used as premises of the rules.

The rules in Fig. 1 are complete for deriving subsumptions between the concepts occurring in the ontology. That is, if O j= C v D for C and D occurring in O, then C v D can be derived using the rules in Fig. 1 [ 13 ]. Therefore, in order to classify the ontology, it is sufficient to compute the closure under the rules and take the derived subsumptions between atomic concepts. This procedure is polynomial since it derives only subsumptions of the form C v D and C v 9R:D where C and D occur in O. Example 1 illustrates the application of rules in Fig. 1 for deriving the entailed subsumption relations.

Example 1. Consider the E L+ ontology O consisting of the following axioms: A v 9R:B; B v 9S:A; 9H:B v C; 9S:C v C; R v H: Then subsumption B v C has the following proof using the rules in Fig. 1. We show the premises used in the inferences in parentheses and side conditions after the colon: A v A Computing the closure under inference rules, such as in Fig. 1, can be performed using a well-known forward chaining procedure detailed in Algorithm 1. The algorithm derives consequences by applying inferences in R and collects those conclusions between saturation(R): input : R: a set of inferences output : S = Closure(R) 1 S; Q ;; 2 for inf 2 R() do 3 Q.add(inf.conclusion); 4 while Q 6= ; do 5 exp Q:takeNext(); 6 if exp 2= S then 7 S.add(exp); 8 for inf 2 R[exp](S) do 9 Q.add(inf.conclusion); 10 return S; /* initialize */

R9 R0

B v B

Rv which all inferences are applied in a set S (the saturation) and the other conclusions in a queue Q. The algorithm first initializes Q with conclusions of the initialization inferences R() R (lines 2–3), and then in a cycle (lines 4–9), repeatedly takes the next expression exp 2 Q, if any, inserts it into S if it does not occur there, and applies all inferences inf 2 R[exp](S) having this expression as one of the premises and other premises from S. The conclusions of such inferences are then inserted back into Q. Note that every inference in R(S) is applied by the algorithm exactly once: this happens in line 8 only when exp is the last premise of the inference added to S. 4

Tracing of Inferences

In this section we describe algorithms for computing the inferences in R deriving given expressions in the closure S under R. Depending on a particular application, one might be interested in computing all inferences for every given expression or just one inference per expression. One might also be interested in unfolding such inferences recursively, that is, computing for each inference also (some or all) inferences deriving its premises. This can be useful for generation of full proofs or for interactive debugging.

Our algorithms are based on ‘tracing of inferences’, that is, we record the relevant inferences during the forward chaining application of the rules. This has an advantage that one can reuse the existing forward chaining infrastructure without requiring additional indexes, e.g., to identify matching premises of the rules by conclusions.

Algorithm 2: Goal-directed tracing of inferences goalDirectedTracing(R; S; Exp): input : Rules: a set of inferences, S, Exp S \ Closure(R(S)): sets of expressions output : M: a multimap from expressions to inferences such that M:Keys = Exp and for each exp 2 Exp we have that M(exp) = R(S)hexpi 1 M; Q ;; 2 for inf 2 R(S n Exp)hExpi do 3 Q.add(inf ); It is relatively straightforward to adapt Algorithm 1 so that all inferences applied in the computation are saved. (cf. [ 11 ] for a formal presentation). Instead of collecting the expressions derived by the inferences in S, we collect the inferences themselves and store them in a multimap M. A multimap is like a map, except that it can store several values (in our case inferences) for the same key (in our case the conclusion of the inferences). The newly found inferences are also processed through the queue Q. If the conclusion of the inference was not derived before by any other inference, it is added to M and all inferences between its conclusion and the previously derived conclusions are produced. Otherwise, we just store the new inference and do nothing else. The algorithm can be easily adapted to store only one traced inference per conclusion: for that it suffices to make M an ordinary map. As Algorithm 1, closure computation with full tracing generates every inference at most once and thus retains polynomial complexity. It might be not practical to store all inferences used in the computation of the closure because this can require much more memory compared to just storing the conclusions of inferences. In practice, one usually does not require all inferences, but just inferences for some conclusions of interest (e.g., resulting from modeling errors). While it is possible to modify full tracing to record only inferences of interest, it is also possible to avoid applying many unnecessary inferences if the closure S under R is already computed.

A goal-directed method for computing R(S)hExpi, that is, the inferences in R(S) that derive expressions from the given set Exp, is detailed in Algorithm 2. The algorithm first generates only those inferences in R(S) that do not use any premises from Exp (lines 2–3), and then repeatedly generates inferences by applying the rules to their conclusions that are in Exp similarly to full tracing. Specifically, the rules are only applied to conclusions of the inferences saved so far (stored in M) and the expressions in S that are not in Exp (see line 9). This is needed to ensure that every inference is generated at most once: an inference inf is generated only when its last premise from Exp is computed. Note that in Algorithm 2 we do not require S to be the closure under R. We just require that Exp is a subset of S and Closure(R(S)), which means that every expression exp 2 Exp must be derivable using only inferences from R restricted to premises in S. The following theorem asserts correctness of the algorithm.

Theorem 1 (Correctness of Algorithm 2). Let R be a set of inferences and S, Exp

S \ Closure(R(S)) be sets of expressions, and M be the output of Algorithm 2 on R; S, and Exp. Then M:Keys = Exp and for each exp 2 Exp we have M(exp) = R(S)hexpi. 4.3

Tracing of Inferences using Partitions

The reader may wonder, why we could not simply iterate over inf 2 R(S)hExpi directly, especially if we could iterate over inf 2 R(S n Exp)hExpi in line 2 of Algorithm 2? In general, iteration over R(S0)hExpi for S0 S can be performed by iterating over all inferences inf 2 R(S0) using a forward chaining procedure similar to full tracing and checking if inf:conclusion 2 Exp. In this case, of course, Algorithm 2 does not give any advantage over full tracing since both algorithms enumerate all inferences in R(S). Algorithm 2, however, gives advantage if R(S n Exp)hExpi is small and can be computed more effectively. For example, in Sect. 5.1, we demonstrate that one can select some non-trivial subsets Exp such that R(S n Exp)hExpi = R()hExpi, that is, only initialization inferences can produce expressions in Exp from expressions not in Exp. If the set of all expressions Exp can be partitioned on such subsets, it is possible to develop a more efficient inference tracing algorithm.

Specifically, let Pts be a fixed countable set of partition identifiers (short partitions), and assume that each expression exp 2 Exp is assigned with exactly one partition exp:partition 2 Pts. Further, let Exp[pt] = fexp 2 Exp j exp:partition = ptg. Then one can use Algorithm 3 to compute R(S)hExpi for arbitrary Exp Exp. Essentially, Algorithm 3 performs tracing of inferences using Algorithm 2 for the partitions assigned to expressions in Exp. This way, one can still enumerate many inferences that do not derive expressions from Exp, but if the partitions are small enough, this overhead is not significant, and the method is still more practical than using full tracing.

Algorithm 3 can be easily modified to trace just one inference per expression and/or to unfold the inferences recursively. For the former, it is sufficient to use the appropriate modification of Algorithm 2 as discussed in Sect. 4.2. For the latter, it is sufficient to repeatedly add the premises for each computed inference with the conclusion in Exp as additional inputs of the algorithm until a fixpoint is reached. 5

Tracing of Inferences in E L+ In this section we apply Algorithm 3 for goal-directed tracing of inferences in E L+ ontologies. To this end, we assume that the closure S under the rules in Fig. 1 is computed, /* by Algorithm 2 */ Algorithm 3: Goal-directed tracing of inferences using partitions goalDirectedPartitionTracing(R; S; Exp): input : R: a set of inferences, S Closure(R(S)), Exp S: sets of expressions output : M: Pts ! Exp ! 2R(S) a two level multimap such that for each exp 2 Exp, we have M(exp:partition)(exp) = R(S)hexpi 1 M ;; 2 for exp 2 Exp do 3 pt exp:partition; 4 if pt 2= M:Keys then 5 M(pt) goalDirectedTracing(R; S; S[pt]) ;

6 return M;

and we are given a set of subsumptions Exp S, for which the inferences that have derived them in S should be found. We first describe our strategy of partitioning the derived subsumptions, then discuss some issues related to optimizations, and, finally, present an empirical evaluation of tracing performance on existing ontologies. To partition the set Exp of concept subsumptions C v D derived by the rules R in Fig. 1, we use the partitioning function used for incremental reasoning in E L+ [ 10 ]. Specifically, the set of partition identifiers Pts is the set of all E L+ concepts, and every subsumption exp = C v D is assigned with the partition exp:partition = C 2 Pts. It is easy to see that each conclusion of a rule in Fig. 1 has the same left-hand side as one of the premises of the rule, unless it is rule R0 or R>. Thus, for the set Exp = S[C] of subsumptions C v D 2 S that belong to partition C, we have R(Exp)hExpi = R()hExpi. Therefore, tracing of inferences for expressions in S[C] can be performed efficiently using Algorithm 2. Note that, according to Algorithm 3, to find all inferences for exp = C v D, it is sufficient to trace just the inferences for partition C. Example 2. Consider subsumptions (1)–(8) derived in Example 1. These subsumptions are assigned to two different partitions A and B. To compute the inferences for B v C, it is sufficient to apply Algorithm 2 for partition B (Exp = Exp[B]) using the precomputed closure S containing (1)–(8). It is easy to see that only inferences for (2), (4), (7), and (8) will be produced by this algorithm (compare Fig. 3 with Fig. 2). During initialization (line 2), Algorithm 2 applies only rule R0 deriving B v B. During closure (line 4), the algorithm applies only inferences to the derived subsumptions in partition B, and keeps only those inferences that produce subsumptions in the same partition. For example, the inference by R9 producing (5) should be ignored, even though it uses a premise B v B from partition B. Note that these inferences would not be computed without S: to produce B v 9S:C we use the premise A v C from S. But we do not need to compute the inferences for A v C first. Thus, the precomputed set S is used in our procedure as a set of support to reach the conclusions of interest as fast as possible.

Now, if we want to unfold the inferences backwards to obtain the full proof for B v C, we need to iterate over the premises that were used to derive B v C and trace their partitions. In our case, B v C was derived from B v 9S:C, for which the partition B was already traced, but continuing further to the premise A v C will bring us to the partition A. When tracing partition A, we produce the remaining inferences for (1), (3), (5), and (6) used in the proof (see Fig. 3). Note that it is not necessary to trace partition A to find the proof, e.g., for B v 9S:A because no expression in partition A was used to derive B v 9S:A. 5.2

Optimizations

In this section we describe how our tracing algorithms can co-exist with known optimizations for E L saturation and present one specific optimization for Algorithm 2 to avoid tracing of unnecessary partitions.

Forward redundancy: Existing implementations of the E L+ procedure based on the rules in Fig. 1, employ a number of additional optimizations to reduce the number of operations. In particular, reasoner ELK avoids applications of some redundant inferences—inferences that are not necessary for obtaining the required consequences. For example, it is not necessary to apply rule Ru to conclusions of rule Ru+, and it is not necessary to apply rules R9 and R if their first premise was derived by rule R9 [ 13 ]. Since the rules are applied by Algorithm 1 only when the conclusion is produced for the first time, the result of the saturation can be different if the rules are applied in a different order. Consequently, if we apply only non-redundant inferences during tracing, due to a potentially different order of rule applications (which may well happen when tracing only partitions), we may miss some of the inferences that were originally applied, and may even fail to derive the expressions to be traced. So, to ensure that all original inferences are traced, we also have to apply the redundant inferences (but if the conclusion of the inference is not in the closure, we do not need to keep it).

Cyclic inferences: As mentioned in Sect. 4.3, Algorithm 3 for tracing inferences using partitions, can be extended to unfold the proofs recursively by repeating the tracing procedure for the premises of relevant inferences. In practice, one is usually interested in minimal proofs, i.e., proofs without repetitions. However, not every inference that is obtained by our procedure can be used in a minimal proof. If an inference is cyclic, that is, some premise of the inference could only be derived from its conclusion, it can be always removed from the proof. Disregarding cyclic inferences can result in fewer traced partitions when unfolding inferences recursively. Note that if we only save the first inference per expression in Algorithm 2, we never create cyclic inferences.

We can avoid many, but not all, cyclic inferences by using a modification of Algorithm 2 in which we save an inference inf in M only if every premise of inf is derived by some inference that does not use the conclusion of inf, i.e., we look only at short cycles. More details and empirical evaluation can be found in the technical report [ 11 ]. We have implemented Algorithm 3 and optimizations described in Sect.s 5.1 and 5.2 in the E L+ reasoner ELK2 and evaluated their performance. We used three large OWL EL ontologies which are often used in evaluations of E L reasoners [ 2, 12, 14 ]: a version of the Gene Ontology (GO),3 an E L+-restricted version of the GALEN ontology,4 and the July 2013 release of SNOMED CT.5 Classification for each experiment was performed with the redundancy optimizations enabled and disabled (the latter eliminates non-determinism and computes all conclusions used in proofs). We used a PC with Intel Core i5-2520M 2.50GHz CPU, with Java 1.6 and 4GB RAM available to JVM.

Full tracing overhead: Our first experiment evaluates the overhead of full tracing (cf. Sect. 4.1 and [ 11 ] for more details) comparing to pure saturation (Algorithm 1). Each ontology was classified 10 times with and without full tracing and the results were averaged (excluding 5 warm-up runs). The results in Table 1 show that there is roughly x2–x4 time overhead as well x3 memory overhead on SNOMED CT when the redundancy elimination is enabled.6 When redundant inferences are applied, the overhead is bigger such that full tracing of SNOMED CT runs out of memory (OOM).

Goal-directed tracing: Next we evaluate performance of goal-directed tracing (Algorithm 3). The experimental setup is as follows: each ontology was classified and then each direct subsumption between concept names was traced with recursive unfolding. Each subsumption was traced independently of others. We separately report results for tracing all of inferences for each conclusion or just of the first inference. The former is useful for generating all proofs whereas the latter can be used to produce one proof. 2http://elk.semanticweb.org 3It is a richer version with concept equivalences, role hierarchies and chains. We thank Chris Mungall from the Lawrence Berkley Lab for providing it. It is accessible at: http://elk.semanticweb.org/ontologies/go_ext.owl.

4http://www.co-ode.org/galen/ 5http://www.ihtsdo.org/snomed-ct/ 6With the smaller ontologies the difference is less observable because of the relatively high (4GB) memory limit set to JVM; the difference is better observable with lower memory limits.

The results are presented in Table 2. First, they demonstrate that the proposed method is very fast as it usually takes around a millisecond to trace a subsumption. (the only exception is SNOMED CT without redundancy elimination, which is likely due to cyclic inferences not detected by the optimization from Sect. 5.2). This is the effect of its goal-directed nature: it only traces inferences which belong to the same partition as an inference used by some proof of the target subsumption. The performance results thus follow from the low number of traced partitions and traced inferences. Second, the algorithm traces more inferences when all proofs are needed but the difference is not substantial and the running times are usually close. This is because alternative proofs overlap and the algorithm rarely needs to trace new partitions when unfolding more than one inference per conclusion. Third, the difference between the number of traced and used inferences shows granularity of partitioning in E L+ (inferences not used in proofs can be traced only if they happen to be in one partition with used inferences). Finally, since the results are averaged over all subsumptions, the reader may wonder if the good performance is because most of them can be proved trivially. Results in the technical report [ 11 ], which are separately aggregated over subsumptions that are provable from at least 10 axioms, show that performance stays on the same level. 6

Summary and Future Research

In this paper we have presented a simple, efficient, and generalizable method for goaldirected tracing of inferences in E L+. Depending on the application, the inferences can be used to recover proofs or compute justifications. The method is goal-directed in the sense that it re-applies only a limited number of inferences using the previously computed conclusions as a set of support. It does not require storing additional indexing information or any sort of bookkeeping during the normal classification. The method is based on the same granularity property of reasoning in E L+ as was previously used for concurrent and incremental reasoning [ 12, 10 ]. Specifically, concept subsumer in E L+ most of the time can be computed independently of each other. This enables efficient partitioning of all derived expressions so that tracing a particular expression requires re-applying inferences only in few partitions, as shown empirically. The same property can be further exploited for other tasks, for example, distributed reasoning in E L+.

References

1. Baader , F. , Brandt , S. , Lutz , C. : Pushing the E L envelope . In: Proc. 19th Int. Joint Conf. on Artificial Intelligence (IJCAI'05) . pp. 364 - 369 ( 2005 )

2. Baader , F. , Lutz , C. , Suntisrivaraporn , B. : Efficient reasoning in E L+ . In: Proc. 2006 Int. Workshop on Description Logics (DL'06) . vol. 189 . CEUR-WS.org ( 2006 )

3. Baader , F. , Peñaloza , R.: Automata-based axiom pinpointing . J. of Automated Reasoning 45 ( 2 ), 91 - 129 ( 2010 )

4. Baader , F. , Peñaloza , R. , Suntisrivaraporn , B. : Pinpointing in the description logic E L . In: Proc. 2007 Int. Workshop on Description Logics (DL'07) . vol. 250 . CEUR-WS.org ( 2007 )

5. Baader , F. , Suntisrivaraporn , B. : Debugging SNOMED CT using axiom pinpointing in the description logic E L+ . In: KR-MED . vol. 410 . CEUR-WS.org ( 2008 )

6. Cuenca Grau , B. , Horrocks , I. , Kazakov , Y. , Sattler , U. : Modular reuse of ontologies: Theory and practice . J. of Artificial Intelligence Research 31 , 273 - 318 ( 2008 )

7. Horridge , M. , Parsia , B. , Sattler , U. : Laconic and precise justifications in OWL . In: Proc. 7th Int. Semantic Web Conf. (ISWC'08) . LNCS, vol. 5318 , pp. 323 - 338 . Springer ( 2008 )

8. Kalyanpur , A. , Parsia , B. , Horridge , M. , Sirin , E.: Finding all justifications of OWL DL entailments . In: Proc. 6th Int. Semantic Web Conf. (ISWC'08) . LNCS, vol. 4825 , pp. 267 - 280 . Springer ( 2007 )

9. Kazakov , Y. : Consequence-driven reasoning for Horn SHIQ ontologies . In: Proc. 21st Int. Joint Conf. on Artificial Intelligence (IJCAI'09) . pp. 2040 - 2045 . IJCAI ( 2009 )

10. Kazakov , Y. , Klinov , P. : Incremental reasoning in OWL EL without bookkeeping . In: Proc. 12th Int. Semantic Web Conf. (ISWC'13) . LNCS, vol. 8218 , pp. 232 - 247 . Springer ( 2013 )

11. Kazakov , Y. , Klinov , P. : Goal-directed tracing of inferences in E L ontologies . Tech. rep. , University of Ulm ( 2014 ), available from http://http://elk.semanticweb.org/ publications/elk-tracing-trdl- 2014 .pdf

12. Kazakov , Y. , Krötzsch , M. , Simancˇík , F.: Concurrent classification of E L ontologies . In: Proc. 10th Int. Semantic Web Conf. (ISWC'11) . LNCS, vol. 7032 , pp. 305 - 320 . Springer ( 2011 )

13. 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 ( 2013 ), to appear

14. 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) . vol. 122 , pp. 45 - 49 ( 2010 )

15. Motik , B. , Shearer , R. , Horrocks , I. : Hypertableau reasoning for description logics . J. of Artificial Intelligence Research 36 , 165 - 228 ( 2009 )

16. Peñaloza , R. , Sertkaya , B. : On the complexity of axiom pinpointing in the E L family of description logics . In: Proc. 12th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR'10) . pp. 280 - 289 . AAAI Press ( 2010 )

17. Reiter , R.: A theory of diagnosis from first principles . Artificial Intelligence 32 ( 1 ), 57 - 95 ( 1987 )

18. Simancˇík , F. , Kazakov , Y. , Horrocks , I. : Consequence-based reasoning beyond Horn ontologies . In: Proc. 22nd Int. Joint Conf. on Artificial Intelligence (IJCAI'11) . pp. 1093 - 1098 . AAAI Press/IJCAI ( 2011 )

19. Sirin , E. , Parsia , B. , Grau , B.C. , Kalyanpur , A. , Katz , Y. : Pellet: A practical OWL-DL reasoner . J. of Web Semantics 5 ( 2 ), 51 - 53 ( 2007 )

20. Tsarkov , D. , Horrocks , I.: FaCT++ description logic reasoner: System description . In: Proc. 3rd Int. Joint Conf. on Automated Reasoning (IJCAR'06) . LNCS, vol. 4130 , pp. 292 - 297 . Springer ( 2006 )