Maximum segments as natural deduction images of some cuts

DOI10.1007/S11787-022-00309-5MaRDI QIDQ2084573zbMATH OpenOpenAlexWikidataFDO

Authors Mirjana Borisavljević

Publication date 18 October 2022

Published in Logica Universalis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s11787-022-00309-5

zbMATH Keywords

natural deductionnormalizationcutssequent systems

Mathematics Subject Classification ID

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

Recommendations

• Normal derivations and sequent derivations
• Connections between cuts and maximum segments
• Sequent calculus in natural deduction style
• Maximum cuts in extended natural deduction
• Minimum segments in sequent derivations

Cites work

• scientific article; zbMATH DE number 1169377 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3333259 (Why is no real title available?)
• A connection between cut elimination and normalization
• A sequent calculus isomorphic to Gentzen's natural deduction
• AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ
• Cut elimination, substitution and normalisation
• Gentzen's Proof of Normalization for Natural Deduction
• Normal derivations and sequent derivations
• Normalization as a consequence of cut elimination
• Normalization as a homomorphic image of cut-elimination
• Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
• Sequent calculus in natural deduction style
• Structural proof theory. With an appendix by Aarne Ranta
• The correspondence between cut-elimination and normalization
• The subformula property of natural deduction derivations and analytic cuts
• The undecidability of k-provability
• Translations from natural deduction to sequent calculus

Cited in

(7)

• Maximum cuts in extended natural deduction
• Connections between cuts and maximum segments
• The elimination of maximum cuts in linear logic and BCK logic
• Minimum segments in sequent derivations
• Normal derivations and sequent derivations
• Sequent images of normal derivations and natural deduction images of derivations without m-cuts
• Graphs of plural cuts

Describes a project that uses

Uses Software

• Pesca

This page was built for publication: Maximum segments as natural deduction images of some cuts

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