Jan 15: G.Mints, Reductions of finite and infinite derivations

Subject: Jan 15: G.Mints, Reductions of finite and infinite derivations
From: Helmut Veith (kgs-owner@dbai.tuwien.ac.at)
Date: Mon Jan 11 1999 - 15:47:49 MET

Lecture Announcement

Gregori Mints
Stanford University

Reductions of finite and infinite derivations
Friday, January 15, 1999, 15:00


One of the main tools of proof-theoretic analysis is a reduction of a
derivation to a normal form by a finite sequence of standard
conversions (cut-elimination steps). For the most intersting
subsystems of analysis complete cut-elimination is possible only for
infinitary versions obtained by adding an omega-rule, say

        From A(n) for all numerals n derive \forall x A(x)

We show how to obtain normalization theorems for finite derivations
from cut-elimination for infinitary derivations.

The construction is based on an alternative view of a pair (D,D_inf)
consisting of a finite derivation D and its standard infinite
expansion D_inf using omega-rules. Namely, D is treated as a finite
encoding of D_inf, and parameters of D (ordinal height, the next
reduction to be applied etc.) are read off D_inf.


Seminarraum SEM 181A, Institut fuer Informationssysteme,
Paniglgasse 16, 1. Stock, 1040 Wien.

Technische Universitaet Wien
Institut fuer Computersprachen E185.2
Resselgasse 3/1, A-1040 Wien

email: mailto:kgs@logic.tuwien.ac.at
listserver: mailto:listproc@dbai.tuwien.ac.at

Mit Unterstuetzung des
Bundesministeriums fuer Wissenschaft und Forschung

This archive was generated by hypermail 2b25 : Thu Apr 06 2000 - 16:19:21 MET DST