Skip to Main content Skip to Navigation
Journal articles

On the decision problem for MELL

Lutz Straßburger 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : In this short paper I will exhibit several mistakes in the recent attempt by Bimbó [3] 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 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 [3], and a semantic proof can be found in [35].
Document type :
Journal articles
Complete list of metadata

Cited literature [46 references]  Display  Hide  Download

https://hal.inria.fr/hal-02386746
Contributor : Lutz Straßburger <>
Submitted on : Friday, November 29, 2019 - 2:31:32 PM
Last modification on : Friday, April 30, 2021 - 9:58:17 AM

File

OnDeciMELL.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Lutz Straßburger. On the decision problem for MELL. Theoretical Computer Science, Elsevier, 2019, 768, pp.91-98. ⟨10.1016/j.tcs.2019.02.022⟩. ⟨hal-02386746⟩

Share

Metrics

Record views

72

Files downloads

262