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.
Type de document :
Communication dans un congrès
WoLLIC 2017 - Logic, Language, Information, and Computation, Jul 2017, London, United Kingdom. 2017
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01635933
Contributeur : Lutz Straßburger <>
Soumis le : mercredi 15 novembre 2017 - 22:20:28
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : vendredi 16 février 2018 - 15:18:07

Fichier

sm-length.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. 2017. 〈hal-01635933〉

Partager

Métriques

Consultations de la notice

115

Téléchargements de fichiers

25