On the Length of Medial-Switch-Mix Derivations

Paola Bruscoli, Lutz Strassburger

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

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.
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
StatusPublished - Jun 2017

Publication series

NameLecture Notes in Computer Science
Volume10388

Fingerprint

Inference Rules
Proof System
Switch
Switches
Associativity
Commutativity
Termination
Modulo
Binary

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. DOI: 10.1007/978-3-662-55386-2_5

On the Length of Medial-Switch-Mix Derivations. / Bruscoli, Paola; Strassburger, Lutz.

Logic, Language and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18–21, 2017: Proceedings. ed. / Juliet Kennedy; Ruy J.G.B. de Queiroz. Berlin, Germany : Springer Verlag, 2017. p. 68-79 (Lecture Notes in Computer Science; Vol. 10388).

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

Bruscoli, P & Strassburger, L 2017, On the Length of Medial-Switch-Mix Derivations. in J Kennedy & RJGB de Queiroz (eds), Logic, Language and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18–21, 2017: Proceedings. Lecture Notes in Computer Science, vol. 10388, Springer Verlag, Berlin, Germany, pp. 68-79. DOI: 10.1007/978-3-662-55386-2_5
Bruscoli P, Strassburger L. On the Length of Medial-Switch-Mix Derivations. In Kennedy J, de Queiroz RJGB, editors, Logic, Language and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18–21, 2017: Proceedings. Berlin, Germany: Springer Verlag. 2017. p. 68-79. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-662-55386-2_5
Bruscoli, Paola ; Strassburger, Lutz. / On the Length of Medial-Switch-Mix Derivations. Logic, Language and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18–21, 2017: Proceedings. editor / Juliet Kennedy ; Ruy J.G.B. de Queiroz. Berlin, Germany : Springer Verlag, 2017. pp. 68-79 (Lecture Notes in Computer Science).
@inproceedings{7a3229d686724b60abed710e2c9fa616,
title = "On the Length of Medial-Switch-Mix Derivations",
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.",
keywords = "Deep Inference, proof complexity, switch-medial, term rewritng",
author = "Paola Bruscoli and Lutz Strassburger",
year = "2017",
month = "6",
doi = "10.1007/978-3-662-55386-2_5",
language = "English",
isbn = "9783662553855",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "68--79",
editor = "Juliet Kennedy and {de Queiroz}, {Ruy J.G.B.}",
booktitle = "Logic, Language and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18–21, 2017",

}

TY - GEN

T1 - On the Length of Medial-Switch-Mix Derivations

AU - Bruscoli,Paola

AU - Strassburger,Lutz

PY - 2017/6

Y1 - 2017/6

N2 - 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.

AB - 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.

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

UR - https://doi.org/10.1007/978-3-662-55386-2_5

U2 - 10.1007/978-3-662-55386-2_5

DO - 10.1007/978-3-662-55386-2_5

M3 - Conference contribution

SN - 9783662553855

T3 - Lecture Notes in Computer Science

SP - 68

EP - 79

BT - Logic, Language and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18–21, 2017

PB - Springer Verlag

CY - Berlin, Germany

ER -