A Sequent Calculus with Implicit Term Representation

9 years 10 months ago
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.
Stefan Hetzl
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CSL
Authors Stefan Hetzl
Comments (0)