Lambek calculus is NP-complete (Q2500488)

The main goal of the paper is to show that the derivability problems for the Lambek calculus (L) and for the Lambek calculus allowing empty premises (L*) are NP-complete. The construction of a reduction from the problem CSAT to the L-derivability and L*-derivability problems is described, and the correctness of this reduction is proved. The proof of one lemma used in the proof of the main results is based on the technique of proof nets. A consequence of the main result of the paper is the NP-completeness of the derivability problem for the multiplicative fragments of cyclic linear logic and noncommutative linear logic. It is the first paper which shows the NP-completeness of derivability for the multiplicative fragments of noncommutative linear logics. A survey of complexity results for commutative linear logic was given by \textit{P. Lincoln} [``Deciding provability of linear logic formulas'', in: J.-Y. Girard et al. (eds.), Advances in linear logic. Based on the linear logic workshop held June 14--18, 1993 at the Mathematical Sciences Institute, Cornell University, Ithaca, New York, USA. Cambridge: Cambridge University Press. Lond. Math. Soc. Lect. Note Ser. 222, 109--122 (1995; Zbl 0823.03004)].