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, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
Sandra Alves and Iliano Cervesato. Proceedings of the Third International Workshop on Linearity, Jul 2014, Vienna, Austria. 176, pp.1--8, 2014, Electronic Proceedings in Theoretical Computer Science. 〈10.4204/EPTCS.176.1〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00998753
Contributeur : Kaustuv Chaudhuri <>
Soumis le : lundi 2 juin 2014 - 16:22:03
Dernière modification le : jeudi 10 mai 2018 - 02:06:32
Document(s) archivé(s) le : mardi 2 septembre 2014 - 12:45:17

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License

Identifiants

Collections

Citation

Kaustuv Chaudhuri. Undecidability of Multiplicative Subexponential Logic. Sandra Alves and Iliano Cervesato. Proceedings of the Third International Workshop on Linearity, Jul 2014, Vienna, Austria. 176, pp.1--8, 2014, Electronic Proceedings in Theoretical Computer Science. 〈10.4204/EPTCS.176.1〉. 〈hal-00998753〉

Partager

Métriques

Consultations de la notice

641

Téléchargements de fichiers

205