Optimising resolution-based rewriting algorithms for OWL ontologies

An important approach to query answering over OWL ontologies is via rewriting   the input ontology (and query) into a new set of axioms that are expressed in logics for which scalable query answering algorithms exist. This approach has been studied for many important fragments of OWL like SHIQSHIQ, Horn-SHIQSHIQ, OWL 2 QL, and OWL 2 EL. An important family of rewriting algorithms is the family of resolution-based algorithms, mostly because of their ability to adapt to any ontology language (such algorithms have been proposed for all aforementioned logics) and the long years of research in resolution theorem-proving. However, this generality comes with performance prices and many approaches that implement algorithms that are tailor-made to a specific language are more efficient than the (usually) general-purposed resolution-based ones.In the current paper we revisit and refine the resolution approaches in order to design efficient rewriting algorithms for many important fragments of OWL. First, we present an algorithm for the language DL-LiteR,⊓R,⊓ which is strongly related to OWL 2 QL. Our calculus is optimised in such a way that it avoids performing many unnecessary inferences, one of the main problems of typical resolution algorithms. Subsequently, we extend the algorithm to the language ELHIELHI which is strongly related to OWL 2 EL. This is a difficult task as ELHIELHI is a relatively expressive language, however, we show that the calculus for DL-LiteR,⊓R,⊓ requires small extensions. Finally, we have implemented all algorithms and have conducted an extensive experimental evaluation using many well-known large and complex OWL ontologies. On the one hand, this is the first evaluation of rewriting algorithms of this magnitude, while, on the other hand, our results show that our system is in many cases several orders of magnitude faster than the existing systems even though it uses an additional backwards subsumption checking step.