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.
 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
 A. Bastenhof, Categorial Symmetry, Ph.D. thesis, Utrecht University (2013).
 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
Financed by the National Centre for Research and Development under grant No. SP/I/1/77065/10 by the strategic scientific research and experimental development program:
SYNAT - “Interdisciplinary System for Interactive Scientific and Scientific-Technical Information”.