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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 1994
Accession Number
ADA289339

Entities

People

  • Frank Pfenning

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Artificial Intelligence
  • Calculus
  • Coding
  • Computer Programming
  • Computer Science
  • Computers
  • Conversion
  • Elimination
  • Hypotheses
  • Judgment
  • Language
  • Logic
  • Notation
  • Programming Languages
  • Reasoning
  • Theoretical Computer Science

Readers

  • Computational Linguistics
  • Parallel and Distributed Computing.