Skip to Main content Skip to Navigation
Conference papers

On the Length of Medial-Switch-Mix Derivations

Paola Bruscoli 1 Lutz Straßburger 2
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Wednesday, November 15, 2017 - 10:20:28 PM
Last modification on : Friday, April 30, 2021 - 10:02:41 AM
Long-term archiving on: : Friday, February 16, 2018 - 3:18:07 PM


Files produced by the author(s)


  • HAL Id : hal-01635933, version 1




Paola Bruscoli, Lutz Straßburger. On the Length of Medial-Switch-Mix Derivations. WoLLIC 2017 - Logic, Language, Information, and Computation, Jul 2017, London, United Kingdom. ⟨hal-01635933⟩



Record views


Files downloads