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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Aarts, E., and K. Trautwein, ‘Non-associative Lambek categorial grammar in polynomial time’, Mathematical Logic Quaterly 41:476-484, 1995.
Abrusci, M., ‘Phase semantics and sequent calculus for pure non-commutative classical linear logic’, Journal of Symbolic Logic 56(4):1403-1451, 1991.
Abrusci, M., and E. Maringelli, ‘A new Correctness Criterion fo Cyclic Multiplicative proof-nets’, Journal of Logic, Language and Information 7(4):449-459, 1998.
Abrusci, M., and P. Ruet, ‘Non commutative logic I: the multiplicative fragment’, Annals of Pure and Applied Logic 101(1):29-64, 2000.
Abrusci, V. M., ‘Non-commutative proof-nets’, in J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, London Mathematical Society Lecture Notes, pages 271-296. Cambridge University Press, 1995.
Berge, C., Graphs, North-Holland, second revised edition edition, 1985.
Buszkowski, W., Logical Foundations of Ajdukiewicz-Lambek Categorial Grammars, Polish Scientific Publishers, 1989 (in Polish).
Buszkowski, W., ‘Generative power of non-associative Lambek Calculus’, Bull. Polish Acad. Sci. Math. 34:507-516, 1986.
de Groote, Ph., ‘A dynamic programming approach to categorial deduction’, in H. Ganzinger, editor, 16th International Conference on Automated Deduction, volume 1632 of Lecture Notes in Artificial Intelligence, pages 1-15. Springer Verlag, 1999.
Fleury, A., La règle d'échange: logique lineaire multiplicative tressée, Thèse de Doctorat, spécialité Mathématiques, Université Paris 7, 1996.
Kandulski, M., ‘The equivalence of nonassociative Lambek categorial grammars and context-free grammars’, Z. Math. Logik Grundlag. Math. 34:103-114, 1988.
Girard, J.-Y., ‘Linear logic’, Theoretical Computer Science 50:1-102, 1987.
Lafont, Y., ‘Interaction nets’, in Proceedings of the 17th ACM symposium on Principles of Programming Languages, ACM Press, 1990.
Lamarche, F., and C. Retoré, ‘Proof nets for the Lambek calculus’, in M. Abrusci and C. Casadio, editors, Proofs and Linguistic Categories, Proceedings 1996 Roma Workshop. Cooperativa Libraria Universitaria Editrice Bologna, 1996.
Lambek, J., ‘The mathematics of sentence structure’, Amer. Math. Monthly, 65:154-170, 1958.
Lambek, J., ‘On the calculus of syntactic types’, in R. Jakobson, editor, Structure of Language and its Mathematical Aspects, pages 166-178, Providence, 1961.
Moortgat, M., ‘Categorial type logic’, in J. van Benthem and A. ter Meulen, editors, Handbook of Logic and Language, chapter 2. Elsevier, 1997.
Puite, Q., and R. Moot, ‘Proof nets for the multimodal Lambek calculus’, Preprint nr. 1096, Department of Mathematics, University of Utrecht, March 1999.
Moortgat, M., and R. Oehrle, ‘Proof nets for the grammatical base logic’, in V. M. Abrusci, C. Casadio, and G. Sandri, editors, Proceedings of the IV Roma Workshop, October 1997. Cooperativa Libraria Universitaria Editrice Bologna, 1999.
Morrill, G., ‘Memoisation of categorial proof nets: parallelism in categorial processing’, in V. M. Abrusci and C. Casadio, editors, Proofs and Linguistic Categories, Proceedings 1996 Roma Workshop. Cooperativa Libraria Universitaria Editrice Bologna, 1996.
Nagayama, M., and M. Okada, ‘A graph-theoretical characterization theorem for multiplicative fragment of non-commutative linear logic’, in J.-Y. Girard, M. Okada, and A. Scedrov, editors, Linear'96, Proceedings of the Tokyo Meeting, volume 3 of Electronic Notes in Theoretical Computer Science. Elsevier-North-Holland, 1996.
Retoré, C., ‘Calcul de Lambek et logique linéaire’, Traitement Automatique des Langues 37(2):39-70, 1997.
Roorda, D., Resource Logics: proof-theoretical investigations. PhD thesis, University of Amsterdam, 1991.
Ruet, P., Logique non-commutative et programmation concurrente par contraintes, Thèse de Doctorat, logique et fondement de l'informatique, Université Denis Diderot, Paris 7, 1997.
Ruet, P., ‘Non commutative logic II: Sequent calculus and phase semantics’, Math. Struc. Comp. Sci. 10(2):277-312.
Szczerba, M., ‘Representation theorems for residuated groupoids’, Proceedings of LACL96, September 1996, Nancy. Springer Lecture Notes in Artificial Intelligence, vol. 1328.
van Benthem, J., Language in Action: Categories, Lambdas and Dynamic Logic, volume 130 of Sudies in Logic and the foundation of mathematics. North-Holland, Amsterdam, 1991.
Yetter, D. N., ‘Quantales and (non-commutative) linear logic’, Journal of Symbolic Logic 55:41-64, 1990.
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
de Groote, P., Lamarche, F. Classical Non-Associative Lambek Calculus. Studia Logica 71, 355–388 (2002). https://doi.org/10.1023/A:1020520915016
Issue Date:
DOI: https://doi.org/10.1023/A:1020520915016