Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus

DOI10.1007/978-3-540-73001-9_41MaRDI QIDQ5425341zbMATH OpenOpenAlexFDO

Authors Kentaro Kikuchi

Publication date 13 November 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73001-9_41

zbMATH Keywords

\(\lambda \)-calculusConfluenceCut-eliminationExplicit substitutionSequent calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05)

Recommendations

• On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
• Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
• Typed Lambda Calculi and Applications

Cited in

(13)

• Indexed systems of sequents and cut-elimination
• From cut-free calculi to automated deduction: the case of bounded contraction
• Restricting Initial Sequents: The Trade-Offs Between Identity, Contraction and Cut
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
• Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
• scientific article; zbMATH DE number 2043517 (Why is no real title available?)
• Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
• Free Definite Description Theory – Sequent Calculi and Cut Elimination
• Herbrand Confluence for First-Order Proofs with Π₂-Cuts
• On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• Typed Lambda Calculi and Applications

This page was built for publication: Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5425341)