A connection between cut elimination and normalization
From MaRDI portal
Publication:818516
DOI10.1007/s00153-005-0295-xzbMath1089.03046OpenAlexW2023487230MaRDI QIDQ818516
Publication date: 21 March 2006
Published in: Archive for Mathematical Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00153-005-0295-x
natural deductionintuitionistic predicate logiccut-elimination theoremconversions for derivationsnormalization theoremsequents
Related Items (4)
AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ Normal derivations and sequent derivations ⋮ Maximum segments as natural deduction images of some cuts
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A cut-elimination proof in intuitionistic predicate logic
- Two measures for proving Gentzen's Hauptsatz without mix
- The correspondence between cut-elimination and normalization
- Normalization as a homomorphic image of cut-elimination
- On permuting cut with contraction
- A proof of Gentzen's \textit{Hauptsatz} without multicut
This page was built for publication: A connection between cut elimination and normalization
