On the Length of Medial-Switch-Mix Derivations - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2017

On the Length of Medial-Switch-Mix Derivations

Résumé

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.
Fichier principal
Vignette du fichier
sm-length.pdf (279 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01635933 , version 1 (15-11-2017)

Identifiants

  • HAL Id : hal-01635933 , version 1

Citer

Paola Bruscoli, Lutz Strassburger. On the Length of Medial-Switch-Mix Derivations. WoLLIC 2017 - Logic, Language, Information, and Computation, Jul 2017, London, United Kingdom. ⟨hal-01635933⟩
120 Consultations
76 Téléchargements

Partager

Gmail Facebook X LinkedIn More