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
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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 : 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)

Identifiers

  • HAL Id : hal-01635933, version 1

Collections

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

200

Files downloads

201