Understanding Resolution Proofs through Herbrand’s Theorem‹

Abstract. 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.