A Structural Proof of Cut Elimination and Its Representation in a Logical Framework,
CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
Pagination or Media Count:
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.
- Computer Hardware