Proof extraction for explanations in defeasible deontic logic

Defeasible deontic logic supports reasoning about obligations and permissions in normative settings. Complete forward-chaining procedures can compute the extension of a theory efficiently, but they do not directly provide user-oriented accounts of why a conclusion holds. In non-monotonic reasoning, however, an explanation cannot consist of a supporting derivation alone: it must also contain information on why the relevant counterarguments do not succeed. In this paper, we address this problem by extracting proof-based explanations from the computation of the extension. We formalize proof trees and proof directed acyclic graph (DAGs) for propositional and deontic conclusions, introduce an annotated dependency graph that records derivation depths during extension computation, and present an extraction algorithm that reconstructs a proof DAG for a queried literal after reasoning terminates. The method extends our previous propositional approach to deontic literals, thus covering conflicts involving obligations and strong permissions as well. For the fragment considered in this paper, namely strong permissions and single-element obligation consequents, we prove that the proof extraction procedure is correct, computable in polynomial time, and yields a depth-minimal proof DAG. We also show how the resulting proof objects can be used as faithful and operationally grounded explanations in simple why-dialogues.