Extraction of Defeasible Proofs as Explanations

Houdini is a Defeasible Deontic Logic reasoner that has been recently developed in Java. The algorithm employed in Houdini follows the proof conditions of the logic to conclude propositional and deontic literals, and is an efficient solution that provides the full extension of a theory. This computation is made in a forward-chaining complete way. Effectiveness is a fundamental property of the adopted approach, but we are also interested in providing an explicit reference to the reasoning that is employed to reach a conclusion. This reasoning is a proof that corresponds to an explanation for that conclusion, and such a proof is less natural to identify in a non-monotonic framework like Defeasible Logic than it would be in a classical one. Depending on the formalism and on the algorithm, the process of reconstructing a proof from a derived conclusion can be cumbersome. Intuitively, a proof consists of a support argument in favour of a literal to be concluded. However, it is necessary also to show that this argument is strong enough, either because the are no arguments against it, or because those arguments are weaker than it. In this paper, with a slight modification of the algorithm of Houdini, we show that it is possible to extract a proof for a defeasible literal in polynomial time, and that such a proof results minimal in its depth.