We intoduce the ELepHant reasoner, a consequence-based reasoner for the EL+ fragment of DLs. We present optimizations, implementation details and experimental results for classi cation of several large bio-medical knowledge bases. In [6, 5] Brandt has shown that the tractability result in [1] for subsumption w.r.t. cyclic E L TBoxes can be extended to the DL E LH, which in addition to E L allows for general concept inclusion axioms and role hierarchies. Later in [2], Baader et. al. have shown that the tractability result can even be further extended to the DL E L++ which in addition to E LH allows for the bottom concept, nominals, role inclusion axioms, and a restricted form of concrete domains. In addition to these promising theoretical results, it turned out that despite their relatively low expressivity, these fragments are still expressive enough for the well-known bio-medical knowledge bases SNOMED [8] and (large parts of) Galen [19], and the Gene Ontology GO [7]. In [3, 4, 21] the practical usability of these fragments on large knowledge bases has been investigated. The CEL Reasoner [18] was as a result of these studies the rst reasoner that could classify the mentioned knowledge bases from the life sciences domain in reasonable times. Successful applications of the E L family increased investment in further work in this direction. The E L family now provides the basis for the pro le OWL2 EL1. Moreover, there are now several other reasoners speci cally tailored for the E L family, like Snorocket [16], TrOWL [22], CB [11] (which extends the E L++ algorithm to Horn SHIQ), JCEL [17] (which is a Java implementation of CEL) and ELK [12, 14, 13, 15] (which is currently the only reasoner that can classify large ontologies from real-life applications within only a few seconds). A comprehensive study comparing the performace of several reasoners on large biomedical knowledge bases has been presented in [9]. A more recent comparison can be found in the experimental results section of [15]. In the present paper we introduce the E LepHant reasoner,2 a consequencebased reasoner for the E L+ fragment of DLs. It is the successor of our prototype reasoner cheetah [20]. Our motivation to develop E LepHant is on the one hand 1 http://www.w3.org/TR/owl2-pro les/#OWL 2 EL 2 http://code.google.com/p/elephant-reasoner
push the performance of OWL EL reasoning further by investigating di erent
optimizations, and on the other hand provide a reasoner with a small footprint
that can be used on platforms with limited memory and computing capabilities
for applications like embedded reasoning [
The paper is organized as follows: After describing the implementation details, we present the results of our experiments for classi cation of large ontologies from the biomedical domain. Although there is still room for improvements like multithreading, the experimental results show that the performance is still promising. 2
The E LepHant reasoner is the successor of the cheetah prototype [
The E LepHant reasoner does not use this method. Instead, it implements
the consequence-based algorithm used in ELK [
As also pointed out in [
One other optimization that E LepHant implements is that it uses the told subsumer information as input axioms for initializing the stack. For each concept name A, instead of using axioms of type A v A as input, it uses A v B, where B is a told subsumer of A.
Apart from these basic optimizations, E LepHant also implements some of
the optimization techniques introduced in [
During saturation, we often need to do a lookup to check if a concept is subsumed by another, or if an axiom has already been processed before, etc. For such operations, we need an e cient data structure. Besides doing a lookup, we also often need to insert new elements to these data structures, like adding a new subsumer to the subsumers list, marking an axiom as processed, etc. But we never delete elements from these data structures. We also sometimes need to iterate over the elements of these data structures. For these operations, the most appropriate data structure is a an associative array. As associative array implementation, we used the Judy array library3 for C. The library is optimized to avoid CPU cache misses as often as possible. Its memory consumption scales smoothly with number of entries, even when the keys are sparsely distributed.
For some of the data structures that are traversed often during saturation, E LepHant keeps double indexes. For instance, the list of subsumers of a concept is stored once as a conventional array and once as Judy array. If during saturation we need to check whether a concept is subsumed by another, we do a lookup in the Judy array. But if we need to traverse the subsumer list, for instance in existential introduction rule, we use the conventional array.
Just like its predecessor, the E LepHant reasoner is implemented in the C programming language. The reason why cheetah was implemented in C is the large amount of memory required by the algorithm that it implements. Due to the large number of concept names and axioms in real-life ontologies, this algorithm requires a large amount of memory and an e cient memory management. This is why we chose C as the implementation language. Although the E LepHant reasoner does not use this algorithm, large part of its code is based on the code of the cheetah prototype. 3
In order to test the performance of E LepHant, we performed a series of experiments on large biomedical knowledge bases from real-life applications. We used the January 2013 international release of SNOMED CT by converting it to OWL functional syntax by the converter provided. Additionally, we used 6 ontologies, namely GO1, FMA, ChEBI, EMAP, Molecule Role and Galen 7 provided in the test ontology suite on the ELK web page.4 We did not use the Galen8, GO2 and Fly Anatomy ontologies provided there since they contain disjointness axioms, 3 http://judy.sourceforge.net 4 http://code.google.com/p/elk-reasoner which is not yet supported by ELepHant. The metrics of the used ontologies are shown in Table 1.
In order to measure the e ects of optimizations described in Section 2, we have run a series of experiments. The experiments were run on a computer with Intel Core i3 processor with 2.1 GHz clock speed, 8 GB of main memory and Linux operating system with 3.2.0 kernel. The results were obtained as average of 5 runs per setting per ontology. We tested the performance gain obtained by using a stack instead of a queue and performance gain obtained by initializing the stack with told subsumer information. Runtimes in miliseconds, and also total and unique number of derivations obtained from these experiments are presented in Table 2. Test results for the setting where a queue is used are marked with 'queue', results for the setting where a stack is used with 'stack' and the results for setting where a stack is used and the stack is initialized with told subsumer information is marked with 'stack+told'. The results show that except for the EMAP and Molecule Role ontologies, using a stack improves the runtime performance even if the number of total or unique derivations does not change. This is due to the overhead of enqueue and dequeue operations compared to the push and pop operations. It is also seen in the table that using the told subsumer information for preparing the input axioms always improves the runtime performance and reduces both the number of total and unique derivations.
We have also run a series of tests for comparing the loading and classi cation performances of ELepHant to that of ELK. We have run ELK 5 times for each ontology with the -XX:+AggressiveHeap parameter and taken the average of these runtimes. The results presented in Table 3 show that ELK classi es the SNOMED CT ontology faster, but needs more time to load it compared to ELepHant. For all smaller ontologies, both classi cation and loading times of ELepHant are slightly shorter. We conjecture that this is due to the overhead of starting the Java virtual machine. In terms of memory usage the performance of ELepHant is quite good as well. For classifying SNOMED CT, the maximum memory usage is around 420MB as the Linux top command shows. For ELK, it is around 1.6GB with the aggressive heap option and around 1GB without this option.
classi cation time total derivations unique derivations
We have introduced the consequence-based E L+ reasoner E LepHant, described implementation details and presented experimental results.
Currently the E LepHant reasoner is still under heavy construction, and there is a number of improvements that we plan to do as future work. First of all, we are going to investigate the role of ordering derived axioms for reducing the number of derivations. We are going to check whether this can be implemented with a feasible overhead. We are going to implement concurrent reasoning in order to further improve the performance. We are going to extend the supported expressivity by allowing disjointness axioms. Last but not least, we are going to implement an OWL API wrapper using the Java native interface in order to make it compatible with ontology editors and other practical applications.