We describe a method for updating the classification of ontologies expressed in the E L family of Description Logics after some axioms have been added or deleted. While incremental classification modulo additions is relatively straightforward, handling deletions is more problematic since it requires retracting logical consequences that no longer hold. Known algorithms address this problem using various forms of bookkeeping to trace the consequences back to premises. But such additional data can consume memory and place an extra burden on the reasoner during application of inferences. In this paper, we present a technique, which avoids this extra cost while being still very efficient for small incremental changes in ontologies.
The E L family of Description Logics (DLs) are tractable extensions of the DL E L featuring conjunction and existential restriction. Despite a limited number of constructors, E L became the language of choice in many applications, especially in Biology and Medicine, which require management of large terminologies. The DL E L++ [1]—an extension of E L with other features such as complex role inclusion axioms, nominals, and datatypes—became the basis of the OWL EL profile [2] of the Web ontology language OWL 2 specifically aimed at such applications.
Ontology classification is one of the main reasoning tasks. It requires computing all entailed (implicit) subsumption relations between atomic concepts. Specialized E L reasoners, such as CEL [3], ELK [4], jcel [5], and Snorocket [6] are able to compute the classification for ontologies as large as SNOMED CT [7] with about 300,000 axioms. Classification plays the key role during ontology development, e.g., for detecting modeling errors that result in mismatches between terms. But even with fast classification procedures, frequent re-classification of ontologies can introduce significant delays in the development workflow, especially as ontologies grow over time.
Several incremental reasoning procedures have been proposed to optimize frequent ontology re-classification after small changes. Most procedures maintain extra information to trace conclusions back to the axioms in order to deal with axiom deletions (see Section 2). Although managing this information typically incurs only a linear overhead, it can be a high cost for large ontologies such as SNOMED CT. In this paper, we propose an incremental reasoning method which does not require computing any such information. The main idea is to split the derived conclusions into several partitions. When some inference used to produce a conclusion in some partition is no longer valid as a result of a deletion, we simply re-compute all conclusions in this partition. Our hypothesis is that, if the number of partitions is sufficiently large and changes are relatively small, the proportion of the partitions affected by changes is small enough, so that re-computation of conclusions is not expensive. We describe a particular partitioning method for E L that does not require storing any additional information, and verify our hypothesis experimentally. Our experiments demonstrate that for large ontologies, such as SNOMED CT, incremental classification can be 10-40 times faster than the (highly optimized) full classification, thus making re-classification almost instantaneous.
In this paper we focus on the DL E L+, which covers most of the existing OWL EL ontologies, and for simplicity, consider only additions and deletions of concept axioms, but not of role axioms. Although the method can be extended to changes in role axioms, it is unlikely to pay off in practice, because such changes are more likely to cause a significant impact on the result of the classification. 2
Directly relevant to this work are various extensions to DL reasoning algorithms to support incremental changes.
Incremental classification in E L modulo additions implemented in the CEL system, comes closest [8]. The procedure works, essentially, by applying new inferences corresponding to the added axioms and closing the set of old and new conclusions under all inference rules. Deletion of axioms is not supported.
Known algorithms that support deletions require a form of bookkeeping to trace conclusions back to the premises. The Pellet reasoner [9] implements a technique called tableau tracing to keep track of the axioms used in tableau inferences [10]. Tracing maps tableau elements (nodes, labels, and relations) to the responsible axioms. Upon deletion of axioms, the corresponding elements get deleted. This method is memoryintensive for large tableaux and currently supports only ABox changes.
The module-based incremental reasoning method does not perform full tracing of inferences, but instead maintains a collection of modules for derived conclusions [11]. The modules consist of axioms in the ontology that entail the respective conclusion, but they are not necessarily minimal. If no axiom in the module was deleted then the entailment is still valid. Unlike tracing, the method does not require changes to the reasoning algorithm, but still incurs the cost of computing and storing the collection of modules.
The approach presented in this paper is closely related to the classical DRed (overdelete, re-derive) strategy for incremental maintenance of recursive views in databases [12]. In the context of ontologies, this method was applied, e.g., for incremental updates of assertions materialized using datalog rules [13], and for stream reasoning in RDF [14]. Just like in DRed, we over-delete conclusions that were derived using deleted axioms (to be on the safe side), but instead of checking which deleted conclusions are still derivable using remaining axioms (which would require additional bookkeeping information), we re-compute some well-defined subset of ‘broken’ conclusions.
In this paper, we will focus on the DL E L+ [3], which can be seen as E L++ [1] without nominals, datatypes, and the bottom concept ?. E L+ concepts are defined using the grammar C ::= A j > j C1 u C2 j 9R:C, where A is an atomic concept, R an atomic role, and C; C1; C2 2 C. E L+ axiom is either a concept inclusion C1 v C2 for C1; C2 2 C, a role inclusion R v S, or a role composition R1 R2 v S, where R; R1; R2; S are atomic roles. E L+ ontology O is a finite set of E L+ axioms. Entailment of axioms by an ontology is defined in a usual way; a formal definition can be found in Appendix A. 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. The ontology classification task requires to compute all entailed subsumptions between atomic concepts occurring in O.
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. 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. The cardinality of the rule R (notation jjRjj) is the number of inferences inf 2 R. Within this paper, we commonly 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 closed under R. Note that the closure 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]) we denote the rule consisting of all inferences inf 2 R such that inf:Premises Exp (respectively Exp inf:Premises). We can combine these operators: for example, R[Exp1](Exp2) consists of those inferences in R whose premises contain all expressions from Exp1 and are a subset of Exp2. Note that this is the same as R(Exp2)[Exp1]. For simplicity, we write R(), R[], R(exp), and R[exp] instead of R(;), R[;], R(fexpg), and R[fexpg] respectively. Note that R[] = R and R() consists of all initialization inferences in R. 3.3
The E L+ reasoning procedure works by applying inference rules to derive subsumptions between concepts. In this paper, we use the rules from E L++ [1] restricted to E L+, but present them in a way that does not require the normalization stage [4].
The rules for E L+ are given in Figure 1, where the premises (if any) are given above the horizontal line, and the conclusions below. Some rules have side conditions R0 C v C : C occurs in O R> C v >
: C and > occur in O 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
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 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, inf:conclusion = C v D1 uD2. 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 Figure 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 Figure 1 [1]. 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. Example 1 in Appendix C demonstrates how to apply the rules in Figure 1 to compute the classification. Computing the closure under inference rules, such as in Figure 1, can be performed using a well-known forward chaining procedure presented in Algorithm 1. The algorithm derives expressions by applying inferences in R and collects those expressions between which all inferences are applied in a set Closure and the remaining ones in a queue Todo. The algorithm first initializes Todo with conclusions of the initialization Algorithm 2: Update modulo additions input : R, R+: sets of inferences, Closure: the closure under R output : Closure: the closure under R [ R+ 1 Todo ; 2 for inf 2 ;(R+ n R)(Closure) do 3 Todo.add(inf.conclusion); 4 R R [ R+; 5 while Todo 6= ; do 6 exp Todo:takeNext(); 7 if exp 2= Closure then 8 Closure.add(exp); 9 for inf 2 R[exp](Closure) do 10 Todo.add(inf.conclusion); 11 return Closure; inferences R() R (lines 2–3), and then in a cycle (lines 4–9), repeatedly takes the next expression exp 2 Todo, if any, inserts it into Closure if it does not occur there, and applies all inferences inf 2 R[exp](Closure) having this expression as one of the premises and other premises from Closure. The conclusions of such inferences are then inserted into Todo. Please see Example 2 in Appendix C illustrating an execution of Algorithm 1.
Let Closure0 be the set computed by Algorithm 1. Note that the algorithm performs as many insertions into Todo as there are inferences in R(Closure0) because every inference inf 2 R(Closure0) is eventually applied, and an inference cannot apply more than once because of line 6. Therefore, the running time of Algorithm 1 can be estimated as O(jjR(Closure0)jj), provided that the initialization inferences inf 2 R() in line 2 and matching inferences inf 2 R[exp](Closure) in line 8 can be effectively enumerated.
In this section, we discuss algorithms for updating the deductive closure under a set of inferences after the set of inferences has changed. Just like in Section 3.4, the material in this section is not specific to any particular inference system, i.e., does not rely on the E L+ classification procedure described in Section 3.3.
The problem of incremental computation of the deductive closure can be formulated as follows. Let R, R+ and R be sets of inferences, and Closure the closure under R. The objective is to compute the closure under the inferences in (R n R ) [ R+, using Closure, R, R+, or R , if necessary. 4.1
If there are no deletions (R = ;), the closure under R [ R+ can be computed by Algorithm 2. Starting from Closure, the closure under R, the algorithm first initializes Algorithm 3: Update modulo deletions (incomplete) input : R, R : sets of inferences, Closure: the closure under R output : Closure: a subset of the closure under (R n R )(Closure) 1 Todo ;; 2 for inf 2 R (Closure) do 3 Todo.add(inf.conclusion); 4 R R n R ; 5 while Todo 6= ; do 6 exp Todo:takeNext();
8 for inf 2 R[exp](Closure) do 9 Todo.add(inf.conclusion); 10
Closure.remove(exp); 11 return Closure; Todo with conclusions of new inferences inf 2 (R+ n R) applicable to Closure, and then processes this queue with respect to the union of all inferences R [ R+ as it is done in Algorithm 1. Note that Algorithm 1 is just a special case of Algorithm 2 when Closure = ; and the initial set of inferences R is empty.
Let Closure be the set in the input of Algorithm 2, and Closure0 the set obtained in the output. Intuitively, the algorithm applies all inferences in (R[R+)(Closure0) that are not in R(Closure) because those should have been already applied. Therefore, the running time of Algorithm 2 can be estimated as O(jj(R [ R+)(Closure0)jj jjR(Closure)jj), which saves us O(jjR(Closure)jj) operations compared to applying Algorithm 1 from scratch. Note that it is essential that we start with the closure under R. If we start with a set that is not closed under R, we may lose conclusions because the inferences in R(Closure) are never applied by the algorithm. Let us now see how to update the closure under deletions, i.e., when R+ = ;. Consider Algorithm 3, which works analogously to Algorithm 2, but removes conclusions instead of adding them. In this algorithm, the queue Todo is used to buffer expressions that should be removed from Closure. We first initialize Todo with consequences of the removed inferences inf 2 R (Closure) (lines 2–3), and then remove such elements together with conclusions of inferences from Closure in which they participate (lines 5–10). Note that in this loop, it is sufficient to consider only consequences under the resulting R = R n R because all consequences under R are already added in Todo during the initialization (lines 2–3).
Unfortunately, Algorithm 3 might not produce the closure under R n R : it may delete expressions that are still derivable in R n R . For example, for the input R = f=a; a=b; b=ag (x=y is an inference with the premise x and conclusion y), R = fb=ag, and Closure = fa; bg, Algorithm 3 removes both a since it is a conclusion of R (Closure), and b since it is a conclusion of (R n R )[a](Closure), yet both a and b are still derivable by the remaining inferences R n R = f=a; a=bg.
A common solution to this problem, is to check, which of the removed expressions are conclusions of the remaining inferences in R(Closure), put them back in Todo, and re-apply the inferences for them like in the main loop of Algorithm 2 (lines 5–10). This is known as the DRed (over-delete, re-derive) strategy in logic programming [12]. But to efficiently check whether an expression is a conclusion of some inference from Closure, one either needs to record how conclusions where produced, or build indexes that help to identify matching premises in Closure by conclusions. Storing this information for everything derived can consume a lot of memory and slow down the inference process.
Note that it makes little sense to ‘simply re-apply’ the remaining inferences in R to the set Closure produced by Algorithm 3. This would require O(jjR(Closure)jj) operations—the same as for computing Closure from scratch using Algorithm 1. Most of the inferences are likely to be already applied to Closure, so, even if it is not ‘fully’ closed under R, it may be ‘almost’ closed. The main idea behind our method presented in the next section, is to identify a large enough subset of expressions Closure1 Closure and a large enough subset of inferences R1 R, such that Closure1 is already closed under R1. We can then re-compute the closure under R incrementally from Closure1 using Algorithm 2 for R+ = R n R1. As has been shown, this approach saves us jjR1(Closure1)jj rule applications compared to computing the closure from scratch.
Let Closure be the set in the input of Algorithm 3, and Closure0 the set obtained in the output. Similarly to Algorithm 2, we can estimate the running time of Algorithm 3 as O(jjR(Closure)jj jj(R n R )(Closure0)jj). Indeed, during initialization (lines 2–3) the algorithm applies all inferences in R (Closure), and in the main loop (lines 5–10) it applies each inference in (R n R )(Closure) that is not in (R n R )(Closure0)—exactly those inferences that have at least one premise in Closure n Closure0. The conclusion of every such inference is removed from Closure, i.e., it is an element of ClosurenClosure0. Although, as has been pointed out, the output Closure0 is not necessarily the closure under R n R , it is, nevertheless, a subset of this closure: Lemma 1. Let Closure be the set in the input of Algorithm 3, and Closure0 the set obtained in the output. Then Closure0 is a subset of the closure under (RnR )(Closure0).
The proof of Lemma 1 can be found in Appendix D.
Note that Lemma 1 claims something stronger than just that Closure0 is a subset of the closure under RnR . It is, in fact, a subset of the closure under (RnR )(Closure0) R n R . Not every subset of the closure under R n R has this property. Intuitively, this property means that every expression in Closure0 can be derived by inferences in R n R using only expressions in Closure0 as intermediate conclusions. This property will be important for correctness of our method.
Our new method for updating the closure under deletions can be described as follows. We partition the set of expressions in Closure on disjoint subsets and modify Algorithm 3 such that whenever an expression is removed from Closure, its partition is Algorithm 4: Repair of over-deletions input : R: a set of inferences, Closure: a subset of the closure under R (Closure), Broken: a set of partitions such that if inf 2 R(Closure) and inf:conclusion 2= Closure then inf:conclusion:partition 2 Broken output : Todo: the conclusions of inferences in R (Closure) that do not occur in Closure 1 Todo; ToRepair; Repaired ;; 2 for inf 2 RhBrokeni(Closure) do 3 if inf:conclusion 2= Closure then 4 Todo.add(inf.conclusion); 5 else 6
ToRepair.add(inf.conclusion); 7 while ToRepair 6= ; do 8 exp ToRepair:takeNext(); 9 if exp 2= Repaired then 10 for inf 2 R[exp](Closure) do 11 if inf:conclusion:partition 2 Broken then 12 if inf:conclusion 2= Closure then 13 Todo.add(inf.conclusion); 14 else 15 ToRepair.add(inf.conclusion); 16
Repaired.add(exp); 17 return Todo; marked as ‘broken’. We then re-apply inferences that can produce conclusions in broken partitions to ‘repair’ the closure.
Formally, let Pts be a fixed countable set of partition identifiers (short partitions), and every expression exp 2 Exp be assigned with exactly one partition exp:partition 2 Pts. For an inference rule R and a set of partitions Pts Pts, let RhPtsi be the set of inferences inf 2 R such that inf:conclusion:partition 2 Pts and exp:partition 2= Pts for every exp 2 inf:Premises. Intuitively, these are all inferences in R that can derive an expression whose partition is in Pts from expressions whose partitions are not in Pts.
We modify Algorithm 3 such that whenever an expression exp is removed from Closure in line 10, we add exp:partition to a special set of partitions Broken. This set is then used to repair Closure in Algorithm 4. The goal of the algorithm is to collect in the queue Todo the conclusions of inferences in R(Closure) that are missing in Closure. This is done by applying all possible inferences inf 2 R(Closure) that can produce such conclusions. There can be two types of such inferences: those whose premises do not belong to any partition in Broken, and those that have at least one such premise. The inferences of the first type are RhBrokeni(Closure); they are applied in initialization (lines 2–6). The inferences of the second type are applied in the main loop of the algorithm (lines 7–16) to the respective expression in Closure whose partition is in Broken.
Whenever an inference inf is applied and inf:conclusion belongs to a partition in Broken (note that it is always the case for inf 2 RhBrokeni(Closure), see also line 11), we check if inf:conclusion occurs in Closure or not. If it does not occur, then we put the conclusion in the output Todo (lines 4, 13). Otherwise, we put it into a special queue ToRepair (lines 6, 15), and repeatedly apply for each exp 2 ToRepair the inferences inf 2 R[exp](Closure) of the second type in the main loop of the algorithm (lines 7–16). After applying all inferences, we move exp into a special set Repaired (line 16), which is there to make sure that we never consider exp again (see line 9).
Lemma 2. Let R, Closure, and Broken be the inputs of Algorithm 4, and Todo the output. Then Todo = finf:conclusion j inf 2 R(Closure)g n Closure.
The proof of Lemma 2 can be found in Appendix D.
After computing the repair Todo of the set Closure using Algorithm 4, we can compute the rest of the closure as in Algorithm 2 using the partially initialized Todo. The correctness of the algorithm follows from Lemma 1, Lemma 2, and the correctness of our modification of Algorithm 2 when Todo is initialized with missing conclusions of R(Closure). The complete algorithm for updating the closure can be found in Appendix B, and its detailed correctness proof in Appendix D.
Algorithm 4 does not impose any restrictions on the assignment of partitions to expressions. Its performance in terms of the number of operations, however, can substantially depend on this assignment. If we assign, for example, the same partition to every expression, then in the main loop (lines 7–16) we have to re-apply all inferences in R(Closure). Thus, it is beneficial to have many different partitions. At another extreme, if we assign a unique partition to every expression, then RhBrokeni would consist of all inferences producing the deleted expressions, and we face the problem of identifying deleted expressions that are still derivable (the conclusions of RhBrokeni(Closure) in lines 2–6). Next, we present a specific partition assignment for the E L+ rules in Figure 1, which circumvents both of these problems. 5 Incremental Reasoning in E L+ In this section, we apply our method for updating the classification of E L+ ontologies computed using the rules in Figure 1. We only consider changes in concept inclusion axioms while resorting to full classification for changes in role inclusions and compositions. We first describe our strategy of partitioning the derived subsumptions, then discuss some issues related to optimizations, and, finally, present an empirical evaluation measuring the performance of our incremental procedure on existing ontologies. The inferences R in Figure 1 operate with concept subsumptions of the form C v D. We partition them into sets of subsumptions having the same left-hand side. Formally, the set of partition identifiers Pts is the set of all E L+ concepts, and every subsumption C v D is assigned to the partition corresponding to its left-hand side C. This assignment provides sufficiently many different partitions (as many as there are concepts in the input ontology) and also has the advantage that the inferences RhPtsi for any set Pts of partitions can be easily identified. Indeed, note that every conclusion of a rule in Figure 1, except for the initialization rules R0 and R>, has the same left-hand side as one of the premises of the rule. Therefore, RhPtsi consists of exactly those inferences in R0 and R> of R for which C 2 Pts. The approach described in Section 4 can be used with any E L+ classification procedure that implements the inference rules in Figure 1 as they are. Existing implementations, however, include a range of further optimizations that avoid unnecessary applications of some rules. For example, it is not necessary to apply Ru to conclusions of Ru+, and it is not necessary to apply R9 and R if its existential premises were obtained by R9 [15]. Even though the closure computed by Algorithm 1 does not change under such optimizations (the algorithm just derives fewer duplicate conclusions), if the same optimizations are used for deletions in Algorithm 3, some deletions could be missed. Intuitively, this happens because the inferences for deleting conclusions in Algorithm 3 can be applied in a different order than they were applied in Algorithm 1 for deriving these conclusions. Please refer to Example 4 in Appendix C demonstrating this situation.
To fix this problem, we do not use rule optimizations for deletions in Algorithm 3. To repair the closure using Algorithm 4, we also need to avoid optimizations to make sure that all expressions in broken partitions of Closure are encountered, but it is sufficient to insert only conclusions of optimized inferences into Todo. We have implemented the procedure described in Section 4.3 in the OWL EL reasoner ELK,1 and performed some preliminary experiments to evaluate its performance. We used three large OWL EL ontologies listed in Table 1 which are frequently used in evaluations of E L reasoners [3–6]: the Gene Ontology GO [16] with 84; 955 axioms, an 1The incremental classification procedure is enabled by default in the latest nightly builds: http://code.google.com/p/elk-reasoner/wiki/GettingElk E L+-restricted version of the GALEN ontology with 36; 547 axioms,2 and the January 2013 release of SNOMED CT with 296; 529 axioms.3
The recent change history of GO is readily available from the public SVN repository.4 We took the last (as of April 2013) 342 changes of GO (the first at r560 with 74; 708 axioms and the last at r7991 with 84; 955 axioms). Each change is represented as sets of added and deleted axioms (an axiom modification counts as one deletion plus one addition). Out of the 9 role axioms in GO, none was modified. Unfortunately, similar data was not available for GALEN or SNOMED CT. We used the approach of Cuenca Grau et.al [11] to generate 250 versions of each ontology with n random additions and deletions (n = 1; 10; 100). For each change history we classified the first version of the ontology and then classified the remaining versions incrementally. All experiments were performed on a PC with Intel Core i5-2520M 2.50GHz CPU, running Java 1.6 with 4GB of RAM available to JVM.
The results of the initial and incremental classifications are given in Table 1 (more details can be found in Appendix E). For GO we have only included results for changes that involve deletions (otherwise the averages for deletion and repair would be artificially lower). First note, that in each case, the incremental procedure makes substantially fewer inferences and takes less time than the initial classification. Unsurprisingly, the difference is most pronounced for larger ontologies and smaller values of n. Also note that the number of inferences in each stage and the number of partitions jBrokenj affected by deletions, depend almost linearly on n, but not the running times. This is because applying several inferences at once is more efficient than separately. Finally, the repair stage takes a relatively small fraction of the total time. 6
In this paper we have presented a new method for incremental classification of E L+ ontologies. It is simple, supports both additions and deletions, and does not require deep modification of the base reasoning procedure (for example, it is implemented in the same concurrent way as the base procedure in ELK [4]). Our experiments, though being preliminary due to the shortage of revision histories for real-life E L ontologies, show that its performance enables nearly real-time incremental updates. Potential applications of the method range from background classification of ontologies in editors to stream reasoning and query answering. The method could also be used to handle ABox changes (via a TBox encoding) or easily extended to consequence-based reasoning procedures for more expressive Description Logics [17, 18].
The main idea of the method is exploiting the granularity of the E L+ reasoning procedure. Specifically, subsumers of concepts can often be computed independently of each other. This property is a corner stone for the concurrent E L classification algorithm used in ELK where contexts are similar to our partitions [4]. In the future, we intend to further exploit this property for on-demand proof generation (for explanation and debugging) and distributed E L reasoning.
2http://www.co-ode.org/galen/ 3http://www.ihtsdo.org/snomed-ct/ 4svn://ext.geneontology.org/trunk/ontology/ 17. Kazakov, Y.: Consequence-driven reasoning for Horn SHIQ ontologies. In Boutilier, C., ed.: Proc. 21st Int. Joint Conf. on Artificial Intelligence (IJCAI’09), IJCAI (2009) 2040–2045 18. Simancˇík, F., Kazakov, Y., Horrocks, I.: Consequence-based reasoning beyond Horn ontologies. In Walsh, T., ed.: Proc. 22nd Int. Joint Conf. on Artificial Intelligence (IJCAI’11), AAAI Press/IJCAI (2011) 1093–1098 This section gives a detailed definition of syntax and semantics of E L+ introduced in Section 3.1. E L+ is defined w.r.t. a vocabulary consisting of countably infinite sets of (atomic) roles and atomic concepts. Complex concepts and axioms are defined recursively in Table 2. We use the letters R; S for roles, C; D; E for concepts, and A; B for atomic concepts. An ontology is a finite set of axioms. Given an ontology O, we write vO for the smallest reflexive transitive binary relation over roles such that R vO S holds for all R v S 2 O.
An interpretation I consists of a nonempty set I called the domain of I and an interpretation function I that assigns to each role R a binary relation RI I
I , and to each atomic concept A a set AI I . This assignment is extended to complex concepts as shown in Table 2. I satisfies an axiom (written I j= ) if the corresponding condition in Table 2 holds. I is a model of an ontology O (written I j= O) if I satisfies all axioms in O. We say that O entails an axiom (written O j= ), if every model of O satisfies .
B
This section presents a detailed description of the method for incremental deductive
closure computation using partitions presented in Section 4.3. The method is described
by Algorithm 5, which consists of three stages:
1. Deletion (lines 2–11): This stage is almost identical to Algorithm 3 except that we
additionally collect in Broken the partitions of the removed expressions (line 11).
2. Repair (
/* ====================== Addition ====================== */ 27 for inf 2 (R+ n R)(Closure) do /* initialize */ 28 Todo.add(inf.conclusion); applying inferences in R(Closure) producing expressions with partitions in Broken. There can be two types of such inferences: those whose premises do not belong to partitions in Broken, and those that have some premises belonging to partitions in Broken. The former inferences will be applied during initialization (lines 12– 16). To implement the latter inferences, we use the queue ToRepair to iterate over those expressions in Closure whose partition is in Broken. Whenever we apply inferences to such expressions, we add them into the set Repaired to make sure we do not consider them again. Every time we derive a conclusion whose partition is in Broken, we either add it into Todo if it does not occur in Closure, or otherwise add it into ToRepair. We then process expressions exp in ToRepair that are not yet in Repaired in a loop (lines 17–26), in which we apply inferences in R[exp](Closure), and insert those conclusions whose partitions are in Broken into Todo or ToRepair similarly as above. 3. Addition (lines 27–35): This stage is identical to Algorithm 2, except that the initial set Closure is not closed under R. But since Todo contains all those conclusions of R(Closure) that do not occur in Closure as ensured by the repair stage, it is guaranteed that all inferences in (R [ R+) will be applied to Closure.
Please see Example 3 in Appendix C illustrating an execution of Algorithm 5 with the partition assignment for E L+ described in Section 5.
C
The following example illustrates the application of rules in Figure 1 for deriving the entailed subsumption relations.
Example 1. Consider the following E L+ ontology O: (ax1): A v 9R:B (ax2): 9H:B v C
(ax3): R v H (ax4): B v 9S:A (ax5): 9S:C v C The subsumptions below can be derived via rules in Figure 1:
A v A B v B
C v C
9R:B v 9R:B
9S:A v 9S:A
9H:B v 9H:B
9S:C v 9S:C
by R0 since A occurs in O,
by R0 since B occurs in O,
(
The following examples illustrate the execution of Algorithm 1 for computing the deductive closure under inferences in Figure 1.
Example 2 (Example 1 continued). The axioms (
The following example illustrates the execution of Algorithm 5 for updating the deductive closure under inferences in Figure 1 using the partition-based approach described in Section 4.3.
Example 3 (Example 1 continued). Let us see how the closure (
During the repair stage, we first need to apply the inferences in RhBrokeni to
Closure (lines 12–16), that is, the instances of R0 for all concepts in Broken except
for 9S:C, which does not occur in O anymore. This adds (
During the addition stage, no inferences will be applied since Todo is empty and
there were no axiom additions. The updated closure, thus, consists of subsumptions
(
The following example demonstrates why some rule optimizations cannot be applied in Algorithm 3 as discussed in Section 5.2.
Example 4. Consider the following E L+ ontology O: (ax1): A v 9R:B (ax2): B v C (ax3): C v B (ax4): 9R:C v 9R:C Let us apply an optimized version of Algorithm 1 for rules in Figure 1, in which we do not apply rule R9 if its left premise is obtained by rule R9:
A v A B v B
C v C
Rule Rv can be further applied to (26) using (ax3), to (27) using (ax2), to (24) using (ax4), and to (28) using (ax4), producing respectively (21), (22), (24), and (28) that have been already derived. Note that (28), (29), and (30) cannot be further used as the left premise of rule R9 because they have been obtained using R9 and we use the optimization that prevents such inferences. But even if we apply such inferences, they produce only subsumptions that are already derived; that is why this optimization does not have any effect on the resulting closure (except for performing fewer inferences).
Assume now that axioms (ax2) and (ax3) are deleted and let us apply Algorithm 3 for the computed set Closure (20)–(30) using the same optimized inference rules. During initialization (lines 2–3) the following inferences for (ax2) and (ax3) will be applied: B v C C v C C v B B v B by Rv to (21) using (ax2), by Rv to (27) using (ax2), by Rv to (22) using (ax3), by Rv to (26) using (ax3).
In the main loop (lines 5–10) for each resulting conclusion that occurs in Closure, the inferences are applied, and the conclusion is deleted from Closure. Assume that this happens in the following order (so far the order in which elements are taken from Todo was not important for correctness of the algorithm): first we process (33): 9R:C v 9R:B by R9 to (24) and (33) using (ax1), by R9 to (28) and (33) using (ax1), (20) (21) (22) (23) (24) (25) (26) (27) (28) (29) (30) (31) (32) (33) (34) (35) after that we process (35), (36), (37), (31), (32), and finally (34).
Note that when processing (35), rule R9 is not applied to (35) and (26) using (ax4) because (35) was obtained using rule R9. Therefore, (24) does not get deleted. Similarly, rule R9 is not applied when processing (36) and (37), so (28) and (30) do not get deleted as well. Since (28) and (30) can only be obtained by rule R9 from (36) and (37), both of which get deleted after processing, the subsumptions (28) and (30) remain in Closure, even though they are not implied by the remaining axioms (ax1) and (ax4). The problem takes place because (28) and (30) were initially obtained by rule R9 from the same premises (23) and (25), but which were derived using different rules (R0 and Rv respectively), to which the existential optimization did not apply.
D
This section presents the omitted proofs of Lemma 1 and Lemma 2, and the correctness proof of Algorithm 5.
Proof of Lemma 1. Let Closure00 be the closure under (R n R )(Closure0). We need to prove that Closure0 Closure00. Clearly, Closure0 Closure and Closure00 Closure. Define Closure1 := (Closure n Closure0) [ Closure00 Closure. We claim that Closure1 is closed under R. Indeed, take any inf 2 R(Closure1). Then there are two possibilities: 1. inf 2 R(Closure) n (R n R )(Closure0): Then inf was applied in Algorithm 3. Therefore, inf:conclusion 2 Closure n Closure0 Closure1. 2. inf 2 (R n R )(Closure0): Since inf 2 R(Closure1) and Closure0 \ Closure1 Closure00, we have inf 2 (R n R )(Closure00). Since Closure00 Closure1 and Closure00 is closed under (R n R )(Closure1), then Closure00 is closed under inf 2 (R n R )(Closure00). Therefore inf:conclusion 2 Closure00 Closure1.
Now, since Closure1 Closure is closed under R and Closure is the smallest set closed under R, we have Closure1 = Closure. Therefore, ; = Closure n Closure1 = Closure0 n Closure00, and so, Closure0 Closure00, as required.
Proof of Lemma 2. Let Closure0 = finf:conclusion j inf 2 R(Closure)g. We need to demonstrate that Todo = Closure0 n Closure. Since Todo Closure0 and Closure \ Todo = ;, it is sufficient to prove that Closure0 n Closure Todo.
First, note that Closure0 is the closure under R(Closure). Indeed, if Closure00 is the closure under R(Closure), then Closure Closure00 by the assumption of Algorithm 4. Hence, for every inf 2 R(Closure) R(Closure00), we have inf:conclusion 2 Closure00. Therefore, Closure0 Closure00, and since Closure0 is closed under R(Closure), we have Closure0 = Closure00.
Let Closure1 = fexp 2 Closure j exp:partition 2= Brokeng. Then it is easy to see from Algorithm 4 that for every inf 2 R(Closure1[Repaired), we have inf:conclusion 2 Closure1 [ Repaired [ Todo. Indeed, if inf:conclusion:partition = Broken then by 2 assumption of Algorithm 4, since inf 2 R(Closure) and inf:conclusion:partition 2= Broken, we must have inf:conclusion 2 Closure, and thus inf:conclusion 2 Closure1.
If inf:conclusion:partition 2 Broken, there are two cases possible. Either inf 2 R(Closure1), thus, inf 2 RhBrokeni(Closure). In this case inf is applied in Algorithm 4 during initialization (lines 2–6). Or, otherwise, inf has at least one premise in Repaired, and hence, it is applied in the main loop of Algorithm 4 (lines 7–16). In both cases the algorithm ensures that inf:conclusion 2 Repaired [ Todo.
Now, since Closure1 [ Repaired [ Todo is closed under R(Closure1 [ Repaired) and Closure \ Todo = ;, it is also closed under R(Closure). Since Closure0 is the closure under R(Closure), we therefore, have Closure0 = Closure1 [Repaired[Todo Closure [ Todo. Hence, Closure0 n Closure Todo, as required.
Theorem 1. Let R, R+, R be the input of Algorithm 5, and Closure3 the set obtained in the output. Then Closure3 is the closure under (R n R ) [ R+.
Proof. Let Closure1 and Broken be the sets obtained after the deletion stage of the algorithm. Then by Lemma 1, for Closure0 the closure under (R n R ), we have Closure1 Closure0. Furthermore, it is easy to see that Broken contains the partitions for all expressions in Closure n Closure1, and, in particular, of those in Closure0 n Closure1 since, obviously, Closure0 Closure.
Let Closure2 and Todo2 be contents of Closure and Todo after the repair stage of Algorithm 5. Clearly, Closure2 = Closure1 since Closure does not change in this stage. Then by Lemma 2, Todo2 consists of all conclusions of (R n R )(Closure2) that do not occur in Closure2. In particular, Todo2 Closure0.
Let Closure00 be the closure under (R n R ) [ R+. Clearly, Closure2 [ Todo2 Closure0 Closure00. Let Closure3 be the content of Closure after the addition stage of Algorithm 5. We need to prove that Closure3 = Closure00. Since in the addition stage, Closure is extended only with content of Todo, which, in turn, can contain only elements of Todo2 or consequences of inferences in R(Closure), we have Closure3 Closure00. We now show that Closure3 is closed under (R n R ) [ R+. For this, take any inference inf 2 ((R n R ) [ R+)(Closure3). We need to prove that inf:conclusion 2 Closure3. There are three cases possible: 1. inf 2 (R n R )(Closure2). Then inf:conclusion 2 Todo2 Closure3. 2. inf 2 (R+ n (R n R ))(Closure2). Then inf:conclusion 2 Closure3 due to the initialization stage of additions (lines 27–28). 3. inf 2 ((R n R ) [ R+)(Closure3) n ((R n R ) [ R+)(Closure2). That is, inf has at least one premise in Closure3 n Closure2. Then inf should be applied in the main loop of the addition stage (lines 30–35). Therefore, inf:conclusion 2 Closure3. Since Closure3 Closure00 is closed under (R n R ) [ R+ and Closure00 is the closure under (R n R ) [ R+, we have Closure3 = Closure00, as required.
E
Table 3 presents the detailed view of the results summarized in Table 1. For each performance metric, the number of inferences or time, it shows the average value as well as the [min–max] interval. In addition, the table presents numbers for the initialization parts of the deletion and addition stages of Algorithm 5 separately since initialization often takes longer than closure. The main reason is that enumeration of all inferences in R (Closure) (resp. (R+ n R)(Closure)) is currently not very efficient. We are investigating some further optimizations of these parts. For the repair stage, initialization and closure are implemented in one loop, as there is only a limited interaction between these parts. Hence we present only the overall figures for this stage.
It can be seen that all three stages (deletion, repair, and addition) exhibit substantial variability in terms of the number of inferences. For the case of GO, this can partly be explained by the varying number of changes, as shown in the first column. For GALEN and SNOMED CT it is explained by the randomness of the change generation algorithm which sometimes picks axioms which affect frequently used concepts in the ontology (and, thus, require more effort during the incremental updates). One can speculate that such changes are less likely to occur during real-life editing process (though to justify this we would need more ontology version data). Also, observe that the dependency of the running time on the number of inferences is non-linear since many inferences are grouped and applied together for performance reasons.