A Connection Between Cut Elimination and Normalization |
| |
Authors: | Mirjana Borisavljević |
| |
Institution: | (1) Faculty of Transport and Traffic Engineering, University of Belgrade, Vojvode Stepe 305, 11000 Belgrade, Serbia and Montenegro |
| |
Abstract: | A new set of conversions for derivations in the system of sequents for intuitionistic predicate logic will be defined. These
conversions will be some modifications of Zucker's conversions from the system of sequents from 11], which will have the following characteristics: (1) these conversions will be sufficient for transforming a derivation
into a cut-free one, and (2) in the natural deduction the image of each of these conversions will be either in the set of
conversions for normalization procedure, or an identity of derivations. This will be used to give a new proof of the normalization
theorem for natural deduction, as a consequence of the cut-elimination theorem for the system of sequents.
Received: January 2003 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|