On the Length of Medial-Switch-Mix Derivations

Paola Bruscoli, Lutz Strassburger

Research output: Chapter in Book/Report/Conference proceedingConference contribution

99 Downloads (Pure)

Abstract

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
Pages68-79
ISBN (Electronic)9783662553862
ISBN (Print)9783662553855
DOIs
Publication statusPublished - Jun 2017

Publication series

NameLecture Notes in Computer Science
Volume10388

    Fingerprint

Keywords

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

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Logic
  • Theoretical Computer Science

Cite this

Bruscoli, P., & Strassburger, L. (2017). On the Length of Medial-Switch-Mix Derivations. In J. Kennedy, & R. J. G. B. de Queiroz (Eds.), Logic, Language and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18–21, 2017: Proceedings (pp. 68-79). (Lecture Notes in Computer Science; Vol. 10388). Berlin, Germany: Springer Verlag. https://doi.org/10.1007/978-3-662-55386-2_5