The elimination of maximum cuts in linear logic and BCK logic

DOI10.1007/s11225-022-10023-4OpenAlexW4311779840MaRDI QIDQ6161950

Mirjana Borisavljević

Publication date: 28 June 2023

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11225-022-10023-4

zbMATH Keywords

normalizationnatural deductioncut-eliminationsystems of sequents

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• A connection between cut elimination and normalization
• Normal derivations and sequent derivations
• The undecidability of \(k\)-provability
• Nonmodal classical linear predicate logic is a fragment of intuitionistic linear logic
• A cut-elimination proof in intuitionistic predicate logic
• A normalizing system of natural deduction for intuitionistic linear logic
• Two measures for proving Gentzen's Hauptsatz without mix
• Linear lambda-terms and natural deduction
• Untersuchungen über das logische Schliessen. II
• Natural deduction for intuitionistic linear logic
• Maximum segments as natural deduction images of some cuts
• A SEQUENT CALCULUS ISOMORPHIC TO GENTZEN’S NATURAL DEDUCTION
• Gentzen's Proof of Normalization for Natural Deduction
• The correspondence between cut-elimination and normalization
• Normalization as a homomorphic image of cut-elimination
• Translations from natural deduction to sequent calculus
• On permuting cut with contraction
• AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ
• The subformula property of natural deduction derivations and analytic cuts
• Cut Elimination, Substitution and Normalisation
• Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation
• A proof of Gentzen's \textit{Hauptsatz} without multicut