Structural Cut Elimination

We present new proofs of cut elimination for intuitionistic, classical, and linear sequent calculi. In all cases the proofs proceed by three nested structural inductions, avoiding the explicit use of multi-sets and termination measures on sequent derivations. This makes them amenable to elegant and concise implementations in Elf, a constraint logic programming language based on the LF logical framework.

• Type: Conference
• Year: 1995
• Where: LICS
• Authors: Frank Pfenning
• Keywords: Automated Reasoning, LF Logical Framework, LICS 1995, Linear Sequent Calculi, Sequent Derivations