Rethinking Explanations: Formalizing Contrast in Description Logics

TL;DR

This paper introduces contrastive explanations for description logic knowledge bases, focusing on why one axiom is true instead of another, addressing user needs and understanding.

Contribution

It formalizes contrastive explanations in description logics and explores their properties, implementation, and evaluation on various knowledge bases.

Findings

Formal foundations of contrasting questions are established.

Contrastive explanations are defined within description logics EL and ALC.

An implementation and experimental evaluation demonstrate practical applicability.

Abstract

There has been a growing interest in explaining entailments over description logic (DL) knowledge bases. The existing explanation formalisms focus on justifications to explain true axioms, and abductive reasoning to explain missing axioms in a knowledge base. However, these formalisms only point out the reasoning steps behind a (missing) entailment and lack a user-centered approach as they do not consider an inquirer's needs, level of understanding, or prior knowledge. We propose contrastive explanations, aiming at answering "why an axiom P (fact) is true instead of another axiom Q (foil)" over description logic knowledge bases. The motivation arises from the observation that when a user discovers that P has occurred, they are often surprised because they anticipated the occurrence of another similar event Q. Furthermore, individual explanations for "why P" and "why not Q" are unsatisfactory since a user expects to see the difference between P and Q. In this work, we first present formal foundations of contrasting questions and then define contrastive explanations within description logics. To this end, facts include ABox assertions of the form C(x) for a concept C and individual x. Possible foils for such facts are assertions C(y) (contrasting against an individual y), or D(x) (contrasting against a concept D). Additionally, we explore the properties of contrastive explanations in the DL EL and ALC. We also provide an implementation of our definition and an experimental evaluation on KBs of varying sizes.