Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation

DOI10.1007/978-94-007-7548-0_2zbMath1339.03051OpenAlexW91833220MaRDI QIDQ5251185

Christian Urban

Publication date: 22 May 2015

Published in: Trends in Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-94-007-7548-0_2

zbMATH Keywords

cut eliminationsequent calculusnormalizationnatural deductionintuitionistic logic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Related Items (6)

AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics ⋮ Prawitz, Proofs, and Meaning ⋮ Cut Elimination, Substitution and Normalisation ⋮ Maximum segments as natural deduction images of some cuts

Cites Work

• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• The correspondence between cut-elimination and normalization
• Normalization as a homomorphic image of cut-elimination
• Lambda terms for natural deduction, sequent calculus and cut elimination
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation