Symmetric normalisation for intuitionistic logic

DOI10.1145/2603088.2603160zbMATH Open1395.03025OpenAlexW2158818713WikidataQ130850193 ScholiaQ130850193MaRDI QIDQ4635630FDOQ4635630

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

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

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)

Cited In (7)

• An intuitionistic formula hierarchy based on high‐school identities
• Strong Cut-Elimination Systems for Hudelmaier’s Depth-Bounded Sequent Calculus for Implicational Logic
• A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs
• Title not available (Why is that?)
• A Local System for Intuitionistic Logic
• Title not available (Why is that?)
• Spinal atomic \(\lambda\)-calculus

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)