Symmetric normalisation for intuitionistic logic

DOI10.1145/2603088.2603160MaRDI QIDQ4635630zbMATHOpenAlexWikidataFDO

Authors Nicolas Guenot, Lutz Straßburger

Publication date 23 April 2018

Published in Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01092105/file/sjs2-final-with-appendix.pdf

zbMATH Keywords

intuitionistic logiccut eliminationdeep inference

Mathematics Subject Classification ID

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

Recommendations

• A Local System for Intuitionistic Logic
• Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
• Cut elimination, substitution and normalisation
• A normalizing system of natural deduction for intuitionistic linear logic
• On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus

Cited in

(7)

• A Local System for Intuitionistic Logic
• Spinal atomic \(\lambda\)-calculus
• scientific article; zbMATH DE number 1941934 (Why is no real title available?)
• An intuitionistic formula hierarchy based on high‐school identities
• scientific article; zbMATH DE number 1302499 (Why is no real title available?)
• A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs
• Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic

This page was built for publication: Symmetric normalisation for intuitionistic logic

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