On the complexsity of some substructural logics.
Wojciech Buszkowski · Reports on Mathematical Logic · 2008
We use a syntactic interpretation of MALL in BCI with ∧, defined in [5], to prove the undecidability of the consequence relations for BCI with ∧ and BCI with ∨, and the NP-completeness of BCI. Similar results are obtained for a variant of the Lambek calculus.