Understanding Resolution Proofs through Herbrand's Theorem

Automated Reasoning with Analytic Tableaux and Related Methods - 22th International Conference, TABLEAUX 2013
Nancy, France


Computer-generated proofs are usually difficult to grasp for a human reader. In this paper we present an approach to understanding resolution proofs through Herbrand’s theorem and the implementation of a tool based on that approach. The information we take as primitive is which instances have been chosen for which quantifiers, in other words: an expansion tree. After computing an expansion tree from a resolution refutation, the user is presented this information in a graphical user interface that allows flexible folding and unfolding of parts of the proof. This interface provides a convenient way to focus on the relevant parts of a computer-generated proof. In this paper, we describe the proof- theoretic transformations, the implementation and demonstrate its use- fulness on several examples.