Concurrent Classification of EL Ontologies


Yevgeny Kazakov, Markus Krötzsch, František Simančík

Concurrent Classification of EL Ontologies

Abstract. We describe an optimised consequence-based procedure for classification of ontologies expressed in a polynomial fragment <math>\mathcal{ELH}_{R^+}</math> of the OWL 2 EL profile. A distinguishing property of our procedure is that it can take advantage of multiple processors/cores, which increasingly prevail in computer systems. Our solution is based on a variant of the "given clause" saturation algorithm for first-order theorem proving, where we assign derived axioms to "contexts" within which they can be used and which can be processed independently. We describe an implementation of our procedure within the Java-based reasoner ELK. Our implementation is light-weight in the sense that an overhead of managing concurrent computations is minimal. This is achieved by employing lock-free data structures and operations such as "compare-and-swap." We report on preliminary experimental results demonstrating a substantial speedup of ontology classification on multi-core systems. In particular, one of the largest and widely-used medical ontologies SNOMED CT can be classified in as little as 5 seconds.

Published at ISWC2011 (Conference paper)

Download PDF (last update: Oct 25 2011)

Citation details


The main reference for ELK is The Incredible ELK. Please use this in citations, as it subsumes and updates most of the material in this conference paper.

There is also an extended technical report that reports the results of this work and that includes experimental data that did not fit the conference publication.

More information about the software used in this paper and pointers to further publications can be found on the page about ELK Reasoner.

Legal notice: This work has been published in Springer LNCS 7032.


Description logics ELK Reasoner