| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
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 con-nectives 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.
Cited literature [22 references]
https://hal.inria.fr/hal-01635933
Contributor : Lutz Straßburger <>
Submitted on : Wednesday, November 15, 2017 - 10:20:28 PM
Last modification on : Thursday, March 5, 2020 - 6:35:40 PM
Long-term archiving on: : Friday, February 16, 2018 - 3:18:07 PM
Contributor : Lutz Straßburger <>
Submitted on : Wednesday, November 15, 2017 - 10:20:28 PM
Last modification on : Thursday, March 5, 2020 - 6:35:40 PM
Long-term archiving on: : Friday, February 16, 2018 - 3:18:07 PM
File
sm-length.pdf
Files produced by the author(s)