Decision Problems for Propositional Non-associative Linear Logic and Extensions

In our previous work, we proposed the logic obtained from full non-associative Lambek calculus by adding a sort of linear-logical modality. We call this logic non-associative non-commutative intuitionistic linear logic ($\mathbf{N}\mathbf{A}\mathbf{C}\mathbf{I}\mathbf{L}\mathbf{L}$, for short). In this paper, we establish the decidability and undecidability results for various extensions of $\mathbf{N}\mathbf{A}\mathbf{C}\mathbf{I}\mathbf{L}\mathbf{L}$. Regarding the decidability results, we show that the deducibility problems for several extensions of $\mathbf{N}\mathbf{A}\mathbf{C}\mathbf{I}\mathbf{L}\mathbf{L}$ with the rule of left-weakening are decidable. Regarding the undecidability results, we show that the provability problems for all the extensions of non-associative non-commutative classical linear logic by the rules of contraction and exchange are undecidable.