On the Length of Medial-Switch-Mix Derivations

Paola Bruscoli; Lutz Strassburger

doi:10.1007/978-3-662-55386-2_5

On the Length of Medial-Switch-Mix Derivations

Paola Bruscoli, Lutz Strassburger

Department of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Citations (Scopus)

158 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 language	English
Title of host publication	Logic, Language and Computation: 24th International Workshop, WoLLIC 2017, London, UK, July 18–21, 2017
Subtitle of host publication	Proceedings
Editors	Juliet Kennedy, Ruy J.G.B. de Queiroz
Place of Publication	Berlin, Germany
Publisher	Springer Verlag
Pages	68-79
ISBN (Electronic)	9783662553862
ISBN (Print)	9783662553855
DOIs	https://doi.org/10.1007/978-3-662-55386-2_5
Publication status	Published - Jun 2017

Publication series

Name	Lecture Notes in Computer Science
Volume	10388

Keywords

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

ASJC Scopus subject areas

Computational Theory and Mathematics
Logic
Theoretical Computer Science

Access to Document

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

sm-length
The final publication is available at Springer via https://doi.org/10.1007/978-3-662-55386-2_5
Accepted author manuscript, 279 KB

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

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). Springer Verlag. https://doi.org/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 proceeding › Conference 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. https://doi.org/10.1007/978-3-662-55386-2_5

@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 = jun,

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

A2 - Kennedy, Juliet

A2 - de Queiroz, Ruy J.G.B.

PB - Springer Verlag

CY - Berlin, Germany

ER -

On the Length of Medial-Switch-Mix Derivations

Abstract

Publication series

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this