AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ

DOI10.1017/S1755020318000102MaRDI QIDQ4577998zbMATH OpenOpenAlexFDO

Authors Mirjana Borisavljević

Publication date 7 August 2018

Published in The Review of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s1755020318000102

zbMATH Keywords

sequent systemsnatural deduction systems

Mathematics Subject Classification ID

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

Recommendations

• Lax orthogonal factorisation systems
• On some orthogonal factorization systems
• Factorization systems as Eilenberg-Moore algebras
• Comprehensive factorisation systems
• An orthogonal approach to algebraic weak factorisation systems

Cites work

• scientific article; zbMATH DE number 1169377 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• scientific article; zbMATH DE number 3348059 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• A connection between cut elimination and normalization
• A natural extension of natural deduction
• A sequent calculus isomorphic to Gentzen's natural deduction
• Cut elimination, substitution and normalisation
• Extended Natural Deduction Images of Conversions from the System of Sequents
• Gentzen's Proof of Normalization for Natural Deduction
• Natural deduction with general elimination rules
• Normalization as a homomorphic image of cut-elimination
• Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
• Structural proof theory. With an appendix by Aarne Ranta
• The correspondence between cut-elimination and normalization
• Translations from natural deduction to sequent calculus

Cited in

(6)

• Normalization as a consequence of cut elimination
• The elimination of maximum cuts in linear logic and BCK logic
• A Note on Gentzen's LJ and NJ Systems Isomorphism
• The subformula property of natural deduction derivations and analytic cuts
• Sequent images of normal derivations and natural deduction images of derivations without m-cuts
• Maximum segments as natural deduction images of some cuts

Describes a project that uses

Uses Software

• Pesca

This page was built for publication: AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ

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