| Abstract |
Knowledge about a complex system represented in ontologies yields a collection of axioms that are too large for human users to browse, let alone to comprehend or reason about it. To this end, we propose a computational framework to zoom in on large ontologies by providing users with either the necessary axioms that act as explanations for sets of entailments, or fix-sized sub-ontologies containing the most relevant information over a vocabulary. First we introduce a new notion, subsumption justification as an extension of justification (a minimal set of axioms needed to preserve a logical consequence) to capture the subsumption knowledge between a term and all other terms in the vocabulary. We present algorithms for computing subsumption justifications based on a simulation notion developed for the problem of deciding the logical difference between ontologies. We show how subsumption justifications can be used to obtain minimal modules and to compute best excerpts by additionally employing a partial Max-SAT solver. This yields two state-of-the-art methods for computing all minimal modules and all best excerpts, which we evaluate over large biomedical ontologies. |