On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
From MaRDI portal
Publication:5387888
Recommendations
- An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
- Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
- Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
- scientific article; zbMATH DE number 874672
- scientific article; zbMATH DE number 1670856
Cited in
(11)- Symmetric normalisation for intuitionistic logic
- Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
- Typed Lambda Calculi and Applications
- Preservation of structural properties in intuitionistic extensions of an inference relation
- An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
- Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic
- Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
- scientific article; zbMATH DE number 1670856 (Why is no real title available?)
- Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
- Strong Normalisation of Cut-Elimination That Simulates β-Reduction
- Cut elimination, substitution and normalisation
This page was built for publication: On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5387888)