Cut elimination, substitution and normalisation

DOI10.1007/978-3-319-11041-7_7MaRDI QIDQ5213610zbMATHOpenAlexFDO

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

zbMATH Keywords

substitutionintuitionistic logicnatural deductioncut eliminationsequent calculusnormalisationminimal logic

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 3889501 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• scientific article; zbMATH DE number 3360143 (Why is no real title available?)
• Extended Natural Deduction Images of Conversions from the System of Sequents
• Higher-order rewrite systems and their confluence
• Natural deduction with general elimination rules
• Nominal techniques in Isabelle/HOL
• Normalization as a homomorphic image of cut-elimination
• On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
• Proofs and computations
• Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
• Strong normalisation of cut-elimination in classical logic
• Structural proof theory. With an appendix by Aarne Ranta
• Term Rewriting and All That
• The correspondence between cut-elimination and normalization
• Untersuchungen über das logische Schliessen. I

Cited in

(13)

• The elimination of maximum cuts in linear logic and BCK logic
• Symmetric normalisation for intuitionistic logic
• Cut-elimination and redundancy-elimination by resolution
• Maximum segments as natural deduction images of some cuts
• Normalization without syntax
• Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs
• Cut rules and explicit substitutions
• scientific article; zbMATH DE number 1471986 (Why is no real title available?)
• Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
• Prawitz, Proofs, and Meaning
• AN ANALYSIS OF THE RULES OF GENTZEN’SNJANDLJ

Describes a project that uses

Uses Software

• Isabelle
• Nominal Isabelle
• Pesca

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)