An adequate compositional encoding of bigraph structure in linear logic with subexponentials

Kaustuv Chaudhuri 1 Giselle Reis 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : In linear logic, formulas can be split into two sets: classical (those that can be used as many times as necessary) or linear (those that are consumed and no longer available after being used). Subexponentials generalize this notion by allowing the formulas to be split into many sets, each of which can then be specified to be classical or linear. This flexibility increases its expressiveness: we already have adequate encodings of a number of other proof systems, and for computational models such as concurrent constraint programming, in linear logic with subexponentials (SEL). Bigraphs were proposed by Milner in 2001 as a model for ubiquitous computing, subsuming models of computation such as CCS and the π-calculus and capable of modeling connectivity and locality at the same time. In this work we present an encoding of the bigraph structure in SEL, thus giving an indication of the expressive power of this logic, and at the same time providing a framework for reasoning and operating on bigraphs. Our encoding is adequate and therefore the operations of composition and juxtaposition can be performed on the logical level. Moreover, all the proof-theoretical tools of SEL become available for querying and proving properties of bigraph structures.
Type de document :
Communication dans un congrès
Martin Davis; Ansgar Fehnker; Annabelle McIver; Andrei Voronkov. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Nov 2015, Suva, Fiji. Springer-Verlag Berlin Heidelberg, 9450, pp.146--161, Lecture Notes in Computer Science. 〈10.1007/978-3-662-48899-7_11〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01208362
Contributeur : Giselle Reis <>
Soumis le : vendredi 2 octobre 2015 - 14:38:20
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : dimanche 3 janvier 2016 - 10:45:31

Fichier

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

Identifiants

Citation

Kaustuv Chaudhuri, Giselle Reis. An adequate compositional encoding of bigraph structure in linear logic with subexponentials. Martin Davis; Ansgar Fehnker; Annabelle McIver; Andrei Voronkov. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Nov 2015, Suva, Fiji. Springer-Verlag Berlin Heidelberg, 9450, pp.146--161, Lecture Notes in Computer Science. 〈10.1007/978-3-662-48899-7_11〉. 〈hal-01208362〉

Partager

Métriques

Consultations de la notice

343

Téléchargements de fichiers

88