Computing minimal subsumption modules of ontologies

In the paper we study algorithms for computing modules that are minimal w.r.t. set inclusion and that preserve the entailment of all subsumptions over a signature of interest. We follow the black-box approach for finding one or all justifications by replacing the entailment tests with logical difference checks, obtaining modules that preserve not only a given consequence but all entailments over a signature. Such minimal modules can serve to improve our understanding of the internal structure of large and complex ontologies. Additionally, several optimisations for speeding up the computation of minimal modules are investigated. We present an experimental evaluation of an implementation of our algorithms for ELH r-terminologies by applying them on the prominent medical ontologies Snomed CT and NCI Thesaurus.