Classical Non Associative Lambek Calculus

Philippe De Groote 1 François Lamarche 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We introduce non-associative linear logic, which may be seen as the classical version of the non-associative Lambek calculus. We define its sequent calculus, its theory of proof nets, for which we give a correctness criterion and a sequentialization theorem, and we show proof search in it is polynomial.
Type de document :
Article dans une revue
Studia Logica, Springer Verlag (Germany), 2002, 71 (3), pp.355-388
Liste complète des métadonnées

https://hal.inria.fr/inria-00100712
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:49:54
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : inria-00100712, version 1

Collections

Citation

Philippe De Groote, François Lamarche. Classical Non Associative Lambek Calculus. Studia Logica, Springer Verlag (Germany), 2002, 71 (3), pp.355-388. 〈inria-00100712〉

Partager

Métriques

Consultations de la notice

86