Model Explanation via Support Graphs

TL;DR

This paper introduces support graphs as a method to explain models of logic programs, establishing their properties and providing an ASP encoding to generate explanations for stable models.

Contribution

It defines support graphs for logic program models, proves properties relating stable and justified models, and offers a meta-programming approach for explanation generation.

Findings

All stable models are justified.

The ASP encoding is sound and complete.

Explanation generation is systematically achievable.

Abstract

In this note, we introduce the notion of support graph to define explanations for any model of a logic program. An explanation is an acyclic support graph that, for each true atom in the model, induces a proof in terms of program rules represented by labels. A classical model may have zero, one or several explanations: when it has at least one, it is called a justified model. We prove that all stable models are justified whereas, in general, the opposite does not hold, at least for disjunctive programs. We also provide a meta-programming encoding in Answer Set Programming that generates the explanations for a given stable model of some program. We prove that the encoding is sound and complete, that is, there is a one-to-one correspondence between each answer set of the encoding and each explanation for the original stable model.