Accession Number : ADA289339

Title :   A Structural Proof of Cut Elimination and Its Representation in a Logical Framework,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s) : Pfenning, Frank

PDF Url : ADA289339

Report Date : NOV 1994

Pagination or Media Count : 68

Abstract : 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.

Descriptors :   *COMPUTER LOGIC, COMPUTATIONS, CALCULI, ELIMINATION, CUTTING.

Subject Categories : Computer Hardware

Distribution Statement : APPROVED FOR PUBLIC RELEASE