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

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

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)

• Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
• Typed Lambda Calculi and Applications
• scientific article; zbMATH DE number 1670856 (Why is no real title available?)
• Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
• Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic
• Symmetric normalisation for intuitionistic logic
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• Preservation of structural properties in intuitionistic extensions of an inference relation
• 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)