This directory contains the Elf implementation of cut elimination
for intuitionistic and classical first-order logic described
in the technical report

  Frank Pfenning.  A structural proof of cut elimination and its
  representation in a logical framework.  Technical Report CMU-CS-94-218,
  Department of Computer Science, Carnegie Mellon University, November 1994.

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.
----------------------------------------------------------------------
formulas.elf --- language definition
int*         --- intuitionistic logic
cl*          --- classical logic
examples.quy --- examples for both intuitionistic and classical logic

CONFIG       --- Elf server configuration file
load.sml     --- SML load file
tokens.elf   --- tokens for Elf to LaTeX conversion
print.elf    --- Elf code to convert Elf source to LaTeX

The printing also requires some supporting LaTeX macros and Emacs Lisp
functions.  Send me mail if you are interested in thos.

Frank Pfenning <fp@cs.cmu.edu>
November 1994