A Sequent Calculus with Implicit Term Representation

We investigate a modification of the sequent calculus which s a first-order proof into its abstract deductive structure and a unifier which renders this structure a valid proof. We define a cutelimination 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.

• Type: Conference
• Year: 2010
• Where: CSL
• Authors: Stefan Hetzl
• Keywords: Automated Reasoning, Calculus, CSL 2010, Sequent Calculus, Standard Calculus