A normalizing system of natural deduction for intuitionistic linear logic

 The main result of this paper is a normalizing system of natural deduction for the full language of intuitionistic linear logic. No explicit weakening or contraction rules for -formulas are needed. By the systematic use of general elimination rules a correspondence between normal derivations and cut-free derivations in sequent calculus is obtained. Normalization and the subformula property for normal derivations follow through translation to sequent calculus and cut-elimination. Received: 10 October 2000 / Revised version: 26 July 2001 / Published online: 2 September 2002 Mathematics Subject Classification (2000): 03F52, 03F05 Keywords or phrases: Linear logic – Natural deduction – General elimination rules