In this paper, we introduce the notion of subsumption justi cation to capture the subsumption knowledge about a term with respect to all primitive and complex concepts built from terms in a given vocabulary . It extends the notion of classical justi cation that is a minimal set of axioms needed to preserve the entailment of a particular subsumption C v D. Then we apply this notion to compute minimal modules [1], i.e., minimal subsets of an ontology that maintain all subsumptions that are formulated in and entailed by the original ontology. We provide two dedicated simulation notions to characterise the set of subsumers and the set of subsumees formulated over a target signature for a given signature term X w.r.t. an E LH-terminology T . The simulation notions originate from the proof-theoretic approach from [4] developed for the problem of deciding the logical di erence between ontologies [2]. Based on the simulation notions, we devise recursive algorithms for extracting the minimal subsets of axioms that preserve the entailments of all -subsumers and all -subsumees of X w.r.t. T . We show that the respective subsumer and subsumee justi cations obtained in this way can then be combined to yield subsumption justi cations. Meanwhile, computing minimal modules equals minimising the union of subsumption justi cations of all concept names in with respect to the ontology. We evaluate a prototype implementation for computing subsumption justications and minimal modules over large biomedical terminologies. The results are encouraging as they show that computing subsumption justi cations is indeed feasible in several important practical cases. In particular, minimal modules can be computed faster using subsumption justi cations than by using the blackbox approach from [1]. The latter is a state-of-the-art approach based on Reiter's Hitting set search algorithm [5] deploying the logical di erence tool CEX [3] for determining whether or not axioms belong to a minimal module.
? This work is partially funded by the ANR project GoAsQ (ANR-15-CE23-0022).