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 metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01635933
Contributor : Lutz Straßburger <>
Submitted on : Wednesday, November 15, 2017 - 10:20:28 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM
Long-term archiving on: Friday, February 16, 2018 - 3:18:07 PM

File

sm-length.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01635933, version 1

Citation

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⟩

Share

Metrics

Record views

182

Files downloads

151