Expressing Additives Using Multiplicatives and Subexponentials

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 subex-ponentials—that are indexed and arranged in a pre-order. Each subexponential has or lacks associated structural properties of weakening and contraction. We show that a classical propositional multiplicative subexponential logic (MSEL) with one unrestricted and two linear subexponentials can encode the halting problem for two register Minsky machines, and is hence undecidable. We then show how the additive con-nectives can be directly simulated by giving an encoding of propositional multiplicative additive linear logic (MALL) in an MSEL with one unrestricted and four linear subexponentials.
Type de document :
Pré-publication, Document de travail
2015
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01222767
Contributeur : Kaustuv Chaudhuri <>
Soumis le : vendredi 30 octobre 2015 - 15:01:14
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : dimanche 31 janvier 2016 - 11:41:02

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

  • HAL Id : hal-01222767, version 1

Citation

Kaustuv Chaudhuri. Expressing Additives Using Multiplicatives and Subexponentials. 2015. 〈hal-01222767〉

Partager

Métriques

Consultations de la notice

354

Téléchargements de fichiers

84