Strong normalization proofs for cut elimination in Gentzen's sequent calculi

Volume 46 / 1999

Elias Bittar Banach Center Publications 46 (1999), 179-225 DOI: 10.4064/-46-1-179-225


We define an equivalent variant $LK_{sp}$ of the Gentzen sequent calculus $LK$. In $LK_{sp}$ weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules $


  • Elias Bittar

Search for IMPAN publications

Query phrase too short. Type at least 4 characters.

Rewrite code from the image

Reload image

Reload image