Herbrand Sequent Extraction

摘要

Computer generated proofs of interesting mathematical theorems are usually too large and full of trivial structural information, and hence hard to understand for humans. Techniques to extract specific essential information from these proofs are needed. In this paper we describe an algorithm to extract Herbrand sequents from proofs written in Gentzen's sequent calculus LK for classical first-order logic. The extracted Herbrand sequent summarizes the creative information of the formal proof, which lies in the instantiations chosen for the quantifiers, and can be used to facilitate its analysis by humans. Furthermore, we also demonstrate the usage of the algorithm in the analysis of a proof of the equivalence of two different definitions for the mathematical concept of lattice, obtained with the proof transformation system CERES.