Accession Number:

ADA289339

Title:

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

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s):

• Pfenning, Frank

Report Date:

1994-11-01

Pagination or Media Count:

68.0

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