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 -