The monotone Lambek calculus is NP-complete

Abstract

We consider the Lambek calculus with the additional structural rule of monotonicity (weakening). We show that the derivability problem for this calculus is NP-complete (both for the full calculus and for the product-free fragment). The same holds for the variant that allows empty antecedents. To prove NP-hardness of the product-free fragment, we provide a mapping reduction from the classical satisfiability problem SAT. This reduction is similar to the one used by Yury Savateev in 2008 to prove NP-hardness (and hence NP-completeness) of the product-free Lambek calculus. © Springer-Verlag Berlin Heidelberg 2014.