Geodesic
An application of proof-nets to the study of fragments of the Lambek calculus
Izvestiya. Mathematics , Tome 75 (2011) no. 3, pp. 631-663.

Voir la notice de l'article provenant de la source Math-Net.Ru

We use proof-nets to study the algorithmic complexity of the derivability problem for some fragments of the Lambek calculus. We prove the NP-completeness of this problem for the unidirectional fragment and the product-free fragment, and also for versions of these fragments that admit empty antecedents.
Keywords: algorithmic complexity, proof-nets.
Mots-clés : Lambek calculus 
@article{IM2_2011_75_3_a7,
     author = {Yu. V. Savateev},
     title = {An application of proof-nets to the study of fragments of the {Lambek} calculus},
     journal = {Izvestiya. Mathematics },
     pages = {631--663},
     publisher = {mathdoc},
     volume = {75},
     number = {3},
     year = {2011},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/IM2_2011_75_3_a7/}
}
TY  - JOUR
AU  - Yu. V. Savateev
TI  - An application of proof-nets to the study of fragments of the Lambek calculus
JO  - Izvestiya. Mathematics 
PY  - 2011
SP  - 631
EP  - 663
VL  - 75
IS  - 3
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/IM2_2011_75_3_a7/
LA  - en
ID  - IM2_2011_75_3_a7
ER  - 
%0 Journal Article
%A Yu. V. Savateev
%T An application of proof-nets to the study of fragments of the Lambek calculus
%J Izvestiya. Mathematics 
%D 2011
%P 631-663
%V 75
%N 3
%I mathdoc
%U http://geodesic.mathdoc.fr/item/IM2_2011_75_3_a7/
%G en
%F IM2_2011_75_3_a7
Yu. V. Savateev. An application of proof-nets to the study of fragments of the Lambek calculus. Izvestiya. Mathematics , Tome 75 (2011) no. 3, pp. 631-663. http://geodesic.mathdoc.fr/item/IM2_2011_75_3_a7/

[1] J. Lambek, “The mathematics of sentence structure”, Amer. Math. Monthly, 65:3 (1958), 154–170 | DOI | MR | Zbl

[2] M. Moortgat, “Categorial type logics”, Handbook of logic and language, North-Holland, Amsterdam; MIT Press, Cambridge, MA, 1997, 93–177 | MR | Zbl

[3] G. V. Morrill, Type logical grammar. Categorial logic of signs, Kluwer Acad. Publ., Dordrecht, 1994 | Zbl

[4] M. Pentus, “Lambek grammars are context free”, Eighth Annual IEEE Symposium on Logic in Computer Science (Montreal, PQ, 1993), IEEE Comput. Soc. Press, Los Alamitos, CA, 1993, 429–433 | DOI | MR

[5] J.-Y. Girard, “Linear logic”, Theoret. Comput. Sci., 50:1 (1987), 1–101 | DOI | MR | Zbl

[6] Ph. de Groote, “The non-associative Lambek calculus with product in polynomial time”, Automated reasoning with analytic tableaux and related methods (Saratoga Springs, NY, USA, 1999), Lecture Notes in Comput. Sci., 1617, Springer-Verlag, Berlin, 1999, 128–139 | DOI | MR | Zbl

[7] E. Aarts, K. Trautwein, “Non-associative Lambek categorial grammar in polynomial time”, Math. Logic Quart., 41:4 (1995), 476–484 | DOI | MR | Zbl

[8] M. Pentus, “Lambek calculus is NP-complete”, Theoret. Comput. Sci., 357:1–3 (2006), 186–201 | DOI | MR | Zbl

[9] Yu. Savateev, “Product-free Lambek calculus is NP-complete”, Logical foundations of computer science. International symposium (Deerfield Beach, FL, USA, 2009), Lecture Notes in Comput. Sci., 5407, Springer-Verlag, Berlin, 2009, 380–394 | DOI | MR | Zbl

[10] Yu. Savateev, “Lambek grammars with one division are decidable in polynomial time”, Computer science – theory and applications (Moscow, Russia, 2008), Lecture Notes in Comput. Sci., 5010, Springer-Verlag, Berlin, 2008, 273–282 | DOI | MR | Zbl

[11] G. Penn, “A graph-theoretic approach to sequent derivability in the Lambek calculus”, Electron. Notes Theor. Comput. Sci., 53 (2004), 274–295 | DOI

[12] A. Lecomte, “Towards efficient parsing with proof-nets”, Proceedings of 6th Conference of the European Chapter of the Association for Computational Linguistics, 1993, 269–276