On the Length of Medial-Switch-Mix Derivations

Paola Bruscoli, Lutz Strassburger

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

3 Citations (SciVal)
220 Downloads (Pure)


Switch and medial are two inference rules that play a central role in many deep inference proof systems. In specific proof systems, the mix rule may also be present. In this paper we show that the maximal length of a derivation using only the inference rules for switch, medial, and mix, modulo associativity and commutativity of the two binary connectives involved, is quadratic in the size of the formula at the conclusion of the derivation. This shows, at the same time, the termination of the rewrite system.
Original languageEnglish
Title of host publicationLogic, Language and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18–21, 2017
Subtitle of host publicationProceedings
EditorsJuliet Kennedy, Ruy J.G.B. de Queiroz
Place of PublicationBerlin, Germany
PublisherSpringer Verlag
ISBN (Electronic)9783662553862
ISBN (Print)9783662553855
Publication statusPublished - Jun 2017

Publication series

NameLecture Notes in Computer Science


  • Deep Inference, proof complexity, switch-medial, term rewritng

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Logic
  • Theoretical Computer Science


Dive into the research topics of 'On the Length of Medial-Switch-Mix Derivations'. Together they form a unique fingerprint.

Cite this