Alex Borgida, Enrico Franconi, Ian Horrocks
The usability of knowledge representation systems, including ones based on Description Logics (DLs) is considerably enhanced by the ability to explain inferences to non-sophisticated users. For DLs, the ability to explain subsumption inferences is particularly useful. This is relatively natural for systems based on structural subsumption algorithms. However, systems that deal with more complex logics, such as ALC, generally use tableaux algorithms, and this does not lead to a natural explanation of subsumption inferences as they are based on ``refutation/unsatisfiability'' proofs of single formulae. We propose using a slightly extended tableaux algorithm that, by keeping track of the ``undesirable'' steps involved in both the reduction of the subsumption problem to an unsatisfiability problem and the normalisation into negation normal form, allows the structure of the original subsumption inference to be preserved. Interestingly, the tableaux proof can be represented as a sequence of rules in a simple variant of sequent calculus. A set of templates are then used to generate "surface" explanations (in one or more steps) from each rule application. The result is a parsimonious yet understandable proof presentation.
Keywords: Description Logics
Citation: Alex Borgida, Enrico Franconi, Ian Horrocks: Explaining ALC Subsumption. In W.Horn (ed.): ECAI2000, Proceedings of the 14th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2000, pp.209-213.