Model-theoretic inseparability and modularity of description logic ontologies

The aim of this paper is to introduce and study model-theoretic notions of modularity in description logic and related reasoning problems. Our approach is based on a generalisation of logical equivalence that is called model-theoretic inseparability. Two TBoxes are inseparable w.r.t. a vocabulary Σ if they cannot be distinguished by the Σ-reducts of their models and thus can equivalently be replaced by one another in any application where only vocabulary items from Σ   are relevant. We study in-depth the complexity of deciding inseparability for the description logics ELEL and ALCALC and their extensions with inverse roles. We then discuss notions of modules of a TBox based on model-theoretic inseparability and develop algorithms for extracting minimal modules from acyclic TBoxes. Finally, we provide an experimental evaluation of our module extraction algorithm based on the large-scale medical TBox Snomed ct.