Abstract
| 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 | |
| Status | Published - Jun 2017 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Volume | 10388 |
Fingerprint
Keywords
- Deep Inference, proof complexity, switch-medial, term rewritng
ASJC Scopus subject areas
- Computational Theory and Mathematics
- Logic
- Theoretical Computer Science
Cite this
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
}
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 -