Undecidability of Multiplicative Subexponential Logic

Kaustuv Chaudhuri
(INRIA)

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.

In Sandra Alves and Iliano Cervesato: Proceedings Third International Workshop on Linearity (LINEARITY 2014), Vienna, Austria, 13th July, 2014, Electronic Proceedings in Theoretical Computer Science 176, pp. 1–8.
Published: 16th February 2015.

ArXived at: http://dx.doi.org/10.4204/EPTCS.176.1 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org