TY - GEN
T1 - On the length of medial-switch-mix derivations
AU - Bruscoli, Paola
AU - Straßburger, Lutz
N1 - Publisher Copyright:
© Springer-Verlag GmbH Germany 2017.
PY - 2017/1/1
Y1 - 2017/1/1
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.
U2 - 10.1007/978-3-662-55386-2_5
DO - 10.1007/978-3-662-55386-2_5
M3 - Conference contribution
AN - SCOPUS:85026741717
SN - 9783662553855
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 68
EP - 79
BT - Logic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings
A2 - Kennedy, Juliette
A2 - de Queiroz, Ruy J.G.B.
PB - Springer Verlag
T2 - 24th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2017
Y2 - 18 July 2017 through 21 July 2017
ER -