Computing OWL ontology decompositions using resolution

Abstract

Reasoning over large ontologies can be done more effectively if they can be decomposed into smaller parts which can be reasoned on independently. This requires identifying parts of the ontology relevant to the problem at hand. We present a novel algorithm, based on resolution calculus, for decomposing an OWL ontology into smaller, more manageable components, such that the union of reasoning over each of these components separately is the same as reasoning over the original ontology. We describe our computational experience using the algorithm, and demonstrate that it is indeed possible to efficiently solve the standard concept subsumption reasoning problem in four large real-world OWL ontologies: SNOMED-CT, NCI, SWEET-JPL and GALEN. We chose SNOMED-CT and NCI because of their size; GALEN because it is highly interconnected; SWEET-JPL because it is expressive (containing negation, both existential and universal quantifiers and both intersections and unions).