Computing Subsumption Justifications of
         Terminologies – Extended Abstract?

           Jieying Chen1 , Michel Ludwig, Yue Ma1 and Dirk Walther
            1
              LRI, Univ. Paris-Sud, CNRS, University Paris-Saclay, France
           {jieying.chen,yue.ma}@lri.fr, {michel.ludwig,dirkww}@gmail.com
    In this paper, we introduce the notion of subsumption justification to capture
the subsumption knowledge about a term with respect to all primitive and com-
plex concepts built from terms in a given vocabulary Σ. It extends the notion
of classical justification 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 sub-
sumers and the set of subsumees formulated over a target signature Σ for a
given signature term X w.r.t. an ELH-terminology T . The simulation notions
originate from the proof-theoretic approach from [4] developed for the problem
of deciding the logical difference 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 justifications
obtained in this way can then be combined to yield subsumption justifications.
Meanwhile, computing minimal modules equals minimising the union of sub-
sumption justifications of all concept names in Σ with respect to the ontology.
    We evaluate a prototype implementation for computing subsumption justi-
fications and minimal modules over large biomedical terminologies. The results
are encouraging as they show that computing subsumption justifications is in-
deed feasible in several important practical cases. In particular, minimal modules
can be computed faster using subsumption justifications than by using the black-
box approach from [1]. The latter is a state-of-the-art approach based on Reiter’s
Hitting set search algorithm [5] deploying the logical difference tool CEX [3] for
determining whether or not axioms belong to a minimal module.

References
1. Chen, J., Ludwig, M., Walther, D.: On computing minimal EL-subsumption mod-
   ules. In: Proceedings of WOMoCoE 2016 (2016)
2. Konev, B., Ludwig, M., Walther, D., Wolter, F.: The logical difference for the
   lightweight description logic EL. JAIR 44, 633–708 (2012)
3. Konev, B., Ludwig, M., Wolter, F.: Logical difference computation with CEX2.5.
   In: Proceedings of IJCAR’12. pp. 371–377 (2012)
4. Ludwig, M., Walther, D.: The logical difference for ELHr-terminologies using hy-
   pergraphs. In: Proceedings of ECAI’14. pp. 555–560 (2014)
5. Reiter, R.: A theory of diagnosis from first principles. AI 32(1), 57–95 (1987)

?
    This work is partially funded by the ANR project GoAsQ (ANR-15-CE23-0022).