A Sequent Calculus with Implicit Term Representation

摘要

We investigate a modification of the sequent calculus which separates a first-order proof into its deductive structure and a unifier which renders this structure a valid proof. We define a cut-elimination procedure for this calculus and show that it produces the same cut-free proofs as the standard calculus, but, due to the implicit representation of terms, it provides exponentially shorter normal forms. This modified calculus is applied as a tool for theoretical analyses of the standard calculus and as a mechanism for a more efficient implementation of cut-elimination.