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

DOI10.1007/11916277_9zbMATH Open1165.03345OpenAlexW1562648369MaRDI QIDQ5387888FDOQ5387888

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

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

Mathematics Subject Classification ID

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

Cited In (9)

• Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
• Typed Lambda Calculi and Applications
• Title not available (Why is that?)
• Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
• Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• Cut Elimination, Substitution and Normalisation
• Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction

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)