Advancing ELK: Not Only Performance Matters

Abstract. This paper reports on the recent development of ELK, a consequence-based reasoner for EL+ ⊥ ontologies. It covers novel reasoning techniques which aim at improving efficiency and providing foundation for new reasoning services. On the former front we present a simple optimization for handling of role com-position axioms, such as transitivity, which substantially reduces the number of rule applications. For the latter, we describe a new rule application strategy that takes advantage of concept definitions to avoid many redundant inferences with-out making rules dependent on derived conclusions. This improvement is not vis-ible to the end user but considerably simplifies implementation for incremental reasoning and proof generation. We also present a rewriting of low-level infer-ences used by ELK to higher-level proofs that can be defined in the standard DL syntax, and thus be used for automatic verification of reasoning results or (vi-sual) ontology debugging. We demonstrate the latter capability using a new ELK Protégé plugin.