This demo will present the advantages of the new, bookkeeping-free method for incremental reasoning in OWL EL on incremental classification of large ontologies.1 In particular, we will show how the typical experience of a user editing a large ontology can be improved if the reasoner (or ontology IDE) provides the capability of instantaneously re-classifying the ontology in the background mode when a change is made. In addition, we intend to demonstrate how incremental reasoning helps in other tasks such as answering DL queries and computing explanations of entailments. We will use our OWL EL reasoner ELK and its Protege plug-in as the main tools to highlight these benefits.
The E L family of Description Logics (DLs) are tractable extensions of the DL E L
featuring conjunction and existential restriction. It is the formal basis of the OWL EL
profile [
The demo will present a novel incremental reasoning procedure implemented in ELK 0.4.0 and its positive impact on re-classification and related reasoning problems.2 1.1
Several incremental reasoning procedures have been developed for ontology languages. Most procedures maintain extra information to trace conclusions back to the axioms in order to deal with axiom deletions.
1This submission complements the accepted research paper which explains the developed
incremental reasoning method in full technical detail [
2A screencast will be available at https://code.google.com/p/elk-reasoner/.
The Pellet reasoner [
The module-based incremental reasoning method does not perform full tracing of
inferences, but instead maintains a collection of modules for derived conclusions [
Managing the extra information such as traces or modules, broadly referred to as bookkeeping, typically incurs only a linear overhead. However, even that can substantially hurt user experience on large ontologies such as SNOMED CT. 1.2
The most frequently occurring scenarios when incremental reasoning is beneficial can be summarized as follows: Continuous Classification The typical ontology development workflow consists of adding, removing, or modifying axioms and occasionally invoking a reasoner to classify the ontology. The latter is done to verify that the changes do not trigger any unwanted entailments and that all desirable entailments are there. Since classification tends to get slower as the ontology grows large, the ontology engineers often do it “offline” after a considerable set of changes has been accumulated. This is sub-optimal because if an error did occur it can become a needle in the haystack to find. A better approach is to classify the ontology continuously in the background mode, i.e., similarly to how modern IDEs continuous compile software’s source code and immediately point out errors. Of course, this approach requires a fast, incremental incorporation of changes. DL Queries Certain applications make use of a form of queries, also called DL Queries, based on complex class expressions. Every DL query is a class expression for which inferred superclasses, subclasses, or individuals need to be computed. One example of such application is the Virtual Fly Brain project.3 DL Queries can be straightforwardly implemented by introducing fresh class names. Suppose superclasses need to be computed for a complex class C. Then one can introduce a fresh class name C0, add the axiom C0 v C to the ontology, and then re-classify it so that C0 finds its place in the class hierarchy. Obviously, the last step is better be implemented incrementally.
This section briefly describes the main aspects of the incremental reasoning procedure implemented in ELK. Full technical details, including the E L+ inference rules, algo
rithms, proofs, and experiments can be found in the research track paper [
There are two main ideas behind our method. The first has been borrowed from
the known DRed (over-delete, re-derive) method for maintaining materialized views in
databases [
A v 9R:B (ax4): 9S:C v C Example 1. Consider the following E L+ ontology O: (ax1): (ax2): 9R:B v C (ax3): (ax5):
C v D
B v 9S:A (ax6): 9S:> v D
One can see that O entails the following atomic subsumptions: A v C, B v C, and B v D (we omit the intermediate inferences). Now, let us see what will happen if (ax4) is deleted. The axiom was used to derive B v C (together with (ax3) and another conclusion A v C) which is retracted first. Then B v D is also deleted since it was produced by an inference which had B v C as a premise (using (ax5)). After that the conclusions whose left hand-side is one of f9S:C; 9S:A; Bg are repaired (intuitively, these are classes whose superclasses changed during the deletion). The repair stage re-applies the inference rules w.r.t. the remaining axioms and restores the conclusion B v D using (ax3) and (ax6). Other conclusions, e.g., for A or C on the left, are intact.
Our experiments demonstrate that in practice the partitioning tends to be pretty fine
and the changes are rather local, i.e., not many partitions need to be repaired. This is
the reason why for large ontologies, such as SNOMED CT, incremental classification is
10–40 times faster than full classification, making re-classification nearly instantaneous
(see [
Finally we describe what we intend to demonstrate during the demo session. Our general goal is to demonstrate performance gains resulted from incremental reasoning to give ontology developers a sense of how their user experience can be improved. 3.1
We will use large ontologies, such SNOMED CT, an E L+ version of GALEN, or others suggested by participants, to demonstrate the sub-second re-classification for a typical ontology editing workflow. We will use the ELK Protege 4+ plug-in5 which allows users
5Available at https://code.google.com/p/elk-reasoner/downloads/list to turn incremental reasoning on and off to highlight the performance differences. We plan to prepare some changesets, including those introducing errors, e.g., class unsatisfiability, but will also let the participants make their own changes to ontology axioms. 3.2
We will demonstrate fast answering of DL queries based on incremental reasoning. For large ontologies, such as SNOMED CT, it will be visible that answering a single query takes considerably less time than re-classification. We plan to use the DL Query plugin for Protege for interactive query answering (so that participants can enter their own queries). To people more interested in answering DL queries via a programming or Web interface, we will show how a simple Web service can handle parallel DL queries posted over HTTP (by computing the corresponding E L saturations incrementally).