Cut elimination, substitution and normalisation
DOI10.1007/978-3-319-11041-7_7zbMATH Open1429.03198OpenAlexW191813668MaRDI QIDQ5213610FDOQ5213610
Authors: 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
Recommendations
- Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
- scientific article; zbMATH DE number 1670856
- An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
- On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
- Cut rules and explicit substitutions
substitutionintuitionistic logicnatural deductioncut eliminationsequent calculusnormalisationminimal logic
Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)
Cites Work
- Nominal techniques in Isabelle/HOL
- Untersuchungen über das logische Schliessen. I
- Structural proof theory. With an appendix by Aarne Ranta
- Title not available (Why is that?)
- Proofs and Computations
- Title not available (Why is that?)
- Title not available (Why is that?)
- Term Rewriting and All That
- Natural deduction with general elimination rules
- Higher-order rewrite systems and their confluence
- The correspondence between cut-elimination and normalization
- Title not available (Why is that?)
- Normalization as a homomorphic image of cut-elimination
- Strong normalisation of cut-elimination in classical logic
- Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
- Title not available (Why is that?)
- Extended Natural Deduction Images of Conversions from the System of Sequents
- Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation
- Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
- On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
Cited In (10)
- Title not available (Why is that?)
- Prawitz, Proofs, and Meaning
- The elimination of maximum cuts in linear logic and BCK logic
- AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ
- An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
- A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs
- Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
- Cut rules and explicit substitutions
- Maximum segments as natural deduction images of some cuts
- Cut-elimination and redundancy-elimination by resolution
Uses Software
This page was built for publication: Cut elimination, substitution and normalisation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5213610)
