An Isomorphism Between Cut-Elimination Procedure and Proof Reduction

DOI10.1007/978-3-540-73228-0_24MaRDI QIDQ3612641zbMATH OpenOpenAlexFDO

Authors Koji Nakazawa

Publication date 10 March 2009

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-73228-0_24

Mathematics Subject Classification ID

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

Recommendations

• On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
• Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
• scientific article; zbMATH DE number 1670856
• scientific article; zbMATH DE number 1722668
• Cut elimination, substitution and normalisation

Cited in

(13)

• Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
• Strong normalization of classical natural deduction with disjunctions
• scientific article; zbMATH DE number 1670856 (Why is no real title available?)
• On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
• Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic
• Preservation of structural properties in intuitionistic extensions of an inference relation
• Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
• Type checking and typability in domain-free lambda calculi
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• scientific article; zbMATH DE number 408808 (Why is no real title available?)
• A Semantic Proof that Reducibility Candidates entail Cut Elimination
• Cut elimination, substitution and normalisation
• On the convergence of reduction-based and model-based methods in proof theory

This page was built for publication: An Isomorphism Between Cut-Elimination Procedure and Proof Reduction

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