Explaining ALC subsumption

Abstract

. Knowledge representation systems, including ones based on Description Logics (DLs), use explanation facilities to, among others, debug knowledge bases. Until now, such facilities were not available for expressive DLs, whose reasoning is an un-natural refutation-based tableau. We offer a solution based on a sequent calculus that is closely related to the tableau implementation, exploiting its optimisations. The resulting proofs are pruned and then presented as simply as possible using templates. 1 Introduction The usability of knowledge representation systems, including ones based on Description Logics (DLs) is considerably enhanced by the ability to explain inferences to knowledge-base developers who are not familiar with the implementation of the reasoner [10]. For DLs, inferring subsumption relationships is a fundamental reasoning task, and its explanation is relatively natural for systems based on structural subsumption algorithms [10]. However, such algorithms are unable to dea...