
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)].
multiplicative fragments, Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics), noncommutative linear logic, derivability, Proof-theoretic aspects of linear logic and other substructural logics, Complexity, Noncommutative linear logic, Theoretical Computer Science, Cyclic linear logic, Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.), Lambek calculus, cyclic linear logic, complexity, Computer Science(all)
multiplicative fragments, Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics), noncommutative linear logic, derivability, Proof-theoretic aspects of linear logic and other substructural logics, Complexity, Noncommutative linear logic, Theoretical Computer Science, Cyclic linear logic, Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.), Lambek calculus, cyclic linear logic, complexity, Computer Science(all)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 60 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 1% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
