On the Decision Problem for MELL

Lutz Straßburger 1
1 PARSIFAL - Proof search and reasoning with logic specifications
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
Abstract : In this short paper I will exhibit several mistakes in the recent attempt by Bimbò to prove the decidability of the multiplicative exponential fragment of linear logic (MELL). In fact, the main mistake is so serious that there is no obvious fix, and therefore the decidability of MELL remains to be an open problem. As a side effect, this paper contains a complete (syntactic) proof of the decidability of the relevant version of MELL (called RMELL in this paper), that is the logic obtained from MELL by replacing the linear logic contraction rule by a general unrestricted version of the contraction rule. This proof can also be found (with a small error) in Bimbò's work, and a semantic proof has been given by Okada and Terui.
Type de document :
Rapport
[Research Report] 9203, Inria Saclay Ile de France. 2018
Liste complète des métadonnées

https://hal.inria.fr/hal-01870148
Contributeur : Lutz Straßburger <>
Soumis le : vendredi 7 septembre 2018 - 11:04:21
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : samedi 8 décembre 2018 - 14:47:39

Fichier

RR-9203.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01870148, version 1

Citation

Lutz Straßburger. On the Decision Problem for MELL. [Research Report] 9203, Inria Saclay Ile de France. 2018. 〈hal-01870148〉

Partager

Métriques

Consultations de la notice

222

Téléchargements de fichiers

90