A connection between cut elimination and normalization

DOI10.1007/S00153-005-0295-XMaRDI QIDQ818516zbMATH OpenOpenAlexFDO

Authors Mirjana Borisavljević

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

zbMATH Keywords

conversions for derivationscut-elimination theoremintuitionistic predicate logicnatural deductionnormalization theoremsequents

Mathematics Subject Classification ID

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

Recommendations

• Extended Natural Deduction Images of Conversions from the System of Sequents
• Normal form theorem for systems of sequents
• Translations from natural deduction to sequent calculus
• Normal derivations and sequent derivations
• Normalization as a consequence of cut elimination

Cites work

• A cut-elimination proof in intuitionistic predicate logic
• A proof of Gentzen's \textit{Hauptsatz} without multicut
• scientific article; zbMATH DE number 1169377 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• Normalization as a homomorphic image of cut-elimination
• On permuting cut with contraction
• The correspondence between cut-elimination and normalization
• Two measures for proving Gentzen's Hauptsatz without mix

Cited in

(13)

• Normal derivations and sequent derivations
• Commuting conversions vs. the standard conversions of the ``good connectives
• Maximum segments as natural deduction images of some cuts
• scientific article; zbMATH DE number 1722668 (Why is no real title available?)
• Normal form theorem for systems of sequents
• Normalization as a consequence of cut elimination
• scientific article; zbMATH DE number 4004176 (Why is no real title available?)
• scientific article; zbMATH DE number 1302506 (Why is no real title available?)
• AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ
• Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
• scientific article; zbMATH DE number 5499335 (Why is no real title available?)
• The elimination of maximum cuts in linear logic and BCK logic
• Sequent images of normal derivations and natural deduction images of derivations without m-cuts

This page was built for publication: A connection between cut elimination and normalization

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q818516)