Explaining ALC Subsumption

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.

• Type: Conference
• Year: 2000
• Where: ECAI
• Authors: Alexander Borgida, Enrico Franconi, Ian Horrocks
• Keywords: Artificial Intelligence, ECAI 2000, Expressive Dls, Knowledge Representation, Un-natural Refutation-based Tableau