The full version of this contribution is available.
This is to announce two papers regarding cut elimination in intuitionistic, classical, and linear logic. They are summarized in: Structural Cut Elimination (extended abstract), Frank Pfenning, December 1994, which is available by anonymous ftp .
All papers are also accessible through WWW .
We present a new proof of cut elimination for linear logic which proceeds by three nested structural inductions, avoiding the explicit use of multi-sets and termination measures on sequent derivations. The computational content of this proof is a non-deterministic algorithm for cut elimination which is amenable to an elegant implementation in Elf. We show this implementation in detail.
We present new proofs of cut elimination for intuitionistic and classical sequent calculi. In both 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 representations in LF, which are given in full detail.