Skip to Main content Skip to Navigation
Conference papers

Undecidability of Multiplicative Subexponential Logic

Kaustuv Chaudhuri 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Subexponential logic is a variant of linear logic with a family of exponential connectives---called subexponentials---that are indexed and arranged in a pre-order. Each subexponential has or lacks associated structural properties of weakening and contraction. We show that classical propositional multiplicative linear logic extended with one unrestricted and two incomparable linear subexponentials can encode the halting problem for two register Minsky machines, and is hence undecidable.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-00998753
Contributor : Kaustuv Chaudhuri <>
Submitted on : Monday, June 2, 2014 - 4:22:03 PM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Tuesday, September 2, 2014 - 12:45:17 PM

Files

main.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - NoDerivatives 4.0 International License

Identifiers

Collections

Citation

Kaustuv Chaudhuri. Undecidability of Multiplicative Subexponential Logic. Proceedings of the Third International Workshop on Linearity, Jul 2014, Vienna, Austria. pp.1--8, ⟨10.4204/EPTCS.176.1⟩. ⟨hal-00998753⟩

Share

Metrics

Record views

917

Files downloads

464