Geodesic
One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
Bulletin of the Section of Logic, Tome 50 (2021) no. 1, pp. 55-80.

Voir la notice de l'article provenant de la source Library of Science

Bilinear Logic of Lambek amounts to Noncommutative MALL of Abrusci. Lambek proves the cut–elimination theorem for a one-sided (in fact, left-sided) sequent system for this logic. Here we prove an analogous result for the nonassociative version of this logic. Like Lambek, we consider a left-sided system, but the result also holds for its right-sided version, by a natural symmetry. The treatment of nonassociative sequent systems involves some subtleties, not appearing in associative logics. We also prove the PTime complexity of the multiplicative fragment of NBL.
Keywords: Substructural logic, Lambek calculus, nonassociative linear logic, sequent system, PTime complexity 
@article{BSL_2021_50_1_a2,
     author = {P{\l}aczek, Pawe{\l}},
     title = {One-Sided {Sequent} {Systems} for {Nonassociative} {Bilinear} {Logic:} {Cut} {Elimination} and {Complexity}},
     journal = {Bulletin of the Section of Logic},
     pages = {55--80},
     publisher = {mathdoc},
     volume = {50},
     number = {1},
     year = {2021},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2021_50_1_a2/}
}
TY  - JOUR
AU  - Płaczek, Paweł
TI  - One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
JO  - Bulletin of the Section of Logic
PY  - 2021
SP  - 55
EP  - 80
VL  - 50
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/BSL_2021_50_1_a2/
LA  - en
ID  - BSL_2021_50_1_a2
ER  - 
%0 Journal Article
%A Płaczek, Paweł
%T One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
%J Bulletin of the Section of Logic
%D 2021
%P 55-80
%V 50
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/BSL_2021_50_1_a2/
%G en
%F BSL_2021_50_1_a2
Płaczek, Paweł. One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity. Bulletin of the Section of Logic, Tome 50 (2021) no. 1, pp. 55-80. http://geodesic.mathdoc.fr/item/BSL_2021_50_1_a2/

[1] V. M. Abrusci, Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic, The Journal of Symbolic Logic, vol. 56(4) (1991), pp. 1403–1451, DOI: http://dx.doi.org/10.2307/2275485

[2] A. Bastenhof, Categorial Symmetry, Ph.D. thesis, Utrecht University (2013).

[3] W. Buszkowski, On classical nonassociative Lambek calculus, [in:] M. Amblard, P. de Groote, S. Pogodalla, C. Retoré (eds.), Logical Aspects of Computational Linguistics, vol. 10054 of Lecture Notes in Computer Science, Springer (2016), pp. 68–84, DOI: http://dx.doi.org/10.1007/978-3-662-53826-5_5

[4] W. Buszkowski, Involutive nonassociative Lambek calculus: Sequent systems and complexity, Bulletin of the Section of Logic, vol. 46(1/2) (2017), DOI: http://dx.doi.org/10.18778/0138-0680.46.1.2.07

[5] P. De Groote, F. Lamarche, Classical non-associative Lambek calculus, Studia Logica, vol. 71(3) (2002), pp. 355–388, DOI: http://dx.doi.org/10.1023/A:1020520915016

[6] N. Galatos, P. Jipsen, Residuated frames with applications to decidability, Transactions of the American Mathematical Society, vol. 365(3) (2013), pp. 1219–1249, URL: https://www.jstor.org/stable/23513444

[7] N. Galatos, H. Ono, Cut elimination and strong separation for substructural logics: an algebraic approach, Annals of Pure and Applied Logic, vol. 161(9) (2010), pp. 1097–1133, DOI: http://dx.doi.org/0.1016/j.apal.2010.01.003

[8] J.-Y. Girard, Linear logic, Theoretical Computer Science, vol. 50(1) (1987), pp. 1–101, DOI: http://dx.doi.org/10.1016/0304-3975(87)90045-4

[9] J. Lambek, On the calculus of syntactic types, [in:] R. Jakobson (ed.), Structure of language and its mathematical aspects, vol. 12, Providence, RI: American Mathematical Society (1961), pp. 166–178, DOI: http://dx.doi.org/10.1090/psapm/012/9972

[10] J. Lambek, Cut elimination for classical bilinear logic, Fundamenta Informaticae, vol. 22(1, 2) (1995), pp. 53–67, DOI: http://dx.doi.org/10.3233/FI-1995-22123

[11] M. Pentus, Lambek calculus is NP-complete, Theoretical Computer Science, vol. 357(1-3) (2006), pp. 186–201, DOI: http://dx.doi.org/10.1016/j.tcs.2006.03.018Get.