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