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.

翻译：本文引入支持图的概念来定义逻辑程序模型的解释。解释是一个无环支持图，对于模型中每个真原子，该图能通过程序规则（以标签表示）诱导出证明。经典模型可能有零个、一个或多个解释：当至少存在一个解释时，该模型被称为合理模型。我们证明所有稳定模型都是合理的，但反之不一定成立，至少对于析取程序而言。此外，我们在回答集编程中提供元编程编码，该编码能为给定程序的稳定模型生成解释。我们证明该编码是可靠且完备的，即编码的每个回答集与原始稳定模型的每个解释之间存在一一对应关系。