Explaining subsumption by optimal interpolation

Abstract

We describe ongoing research to support the construction of terminologies with Description Logics. For the explanation of subsumption we search for particular concepts because of their syntactic and semantic properties. More precisely, the set of explanations for a subsumption P=Nis the set of optimal interpolants for P and N. We provide definitions for optimal interpolation and an algorithm based on Boolean minimisation of concept-names in a tableau proof for ALC-satisfiability Finally, we describe our implementation and some experiments to assess the computational scalability of our proposal.