Cut Elimination, Substitution and Normalisation

DOI10.1007/978-3-319-11041-7_7zbMath1429.03198OpenAlexW191813668MaRDI QIDQ5213610

Roy Dyckhoff

Publication date: 4 February 2020

Published in: Dag Prawitz on Proofs and Meaning (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/10023/7962

zbMATH Keywords

cut eliminationsequent calculusnatural deductionintuitionistic logicnormalisationsubstitutionminimal logic

Mathematics Subject Classification ID

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

Related Items (4)

AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ ⋮ The elimination of maximum cuts in linear logic and BCK logic ⋮ Prawitz, Proofs, and Meaning ⋮ Maximum segments as natural deduction images of some cuts

Uses Software

• Isabelle
• Nominal Isabelle
• Pesca

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Nominal techniques in Isabelle/HOL
• Higher-order rewrite systems and their confluence
• Natural deduction with general elimination rules
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Untersuchungen über das logische Schliessen. I
• Proofs and Computations
• The correspondence between cut-elimination and normalization
• Normalization as a homomorphic image of cut-elimination
• Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
• Extended Natural Deduction Images of Conversions from the System of Sequents
• Term Rewriting and All That
• Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation
• On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus

This page was built for publication: Cut Elimination, Substitution and Normalisation