Symmetric normalisation for intuitionistic logic

Nicolas Guenot, Lutz Straßburger

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


We present two proof systems for implication-only intuitionistic logic in the calculus of structures. The first is a direct adaptation of the standard sequent calculus to the deep inference setting, and we describe a procedure for cut elimination, similar to the one from the sequent calculus, but using a non-local rewriting. The second system is the symmetric completion of the first, as normally given in deep inference for logics with a DeMorgan duality: all inference rules have duals, as cut is dual to the identity axiom. We prove a generalisation of cut elimination, that we call symmetric normalisation, where all rules dual to standard ones are permuted up in the derivation. The result is a decomposition theorem having cut elimination and interpolation as corollaries.
Original languageEnglish
Title of host publicationJoint 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), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014
EditorsThomas A. Henzinger, Dale Miller
Number of pages10
PublisherAssociation for Computing Machinery
Publication date12 Sept 2014
ISBN (Print)978-1-4503-2886-9
Publication statusPublished - 12 Sept 2014


  • Deep inference
  • Intuitionistic logic
  • Cut elimination


Dive into the research topics of 'Symmetric normalisation for intuitionistic logic'. Together they form a unique fingerprint.

Cite this