On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus

DOI10.1007/11916277_9MaRDI QIDQ5387888zbMATH OpenOpenAlexFDO

Authors Kentaro Kikuchi

Publication date 27 May 2008

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11916277_9

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Cut-elimination and normal-form theorems (03F05)

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

(12)

• Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
• scientific article; zbMATH DE number 1670856 (Why is no real title available?)
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic
• Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
• Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
• Symmetric normalisation for intuitionistic logic
• Preservation of structural properties in intuitionistic extensions of an inference relation
• Cut elimination, substitution and normalisation
• Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• Typed Lambda Calculi and Applications

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)