Explaining Non-Entailment by Model Transformation for the Description Logic EL

Reasoning results computed by description logic systems can be hard to comprehend. When an ontology does not entail an expected subsumption relationship, generating an explanation of this non-entailment becomes necessary. In this paper, we use countermodels to explain non-entailments. More precisely, we devise relevant parts of canonical models of ontologies that serve as explanations and discuss the computational complexity of extracting these parts by means of model transformations. Furthermore, we provide an implementation of these transformations and evaluate it using real ontologies.