Cut Elimination, Substitution and Normalisation
From MaRDI portal
Publication:5213610
DOI10.1007/978-3-319-11041-7_7zbMath1429.03198OpenAlexW191813668MaRDI QIDQ5213610
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
cut eliminationsequent calculusnatural deductionintuitionistic logicnormalisationsubstitutionminimal logic
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
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