Complexity of the Lambek calculus with one division and a negative-polarity modality for weakening

In this paper, we consider a variant of the Lambek calculus allowing empty antecedents. This variant uses two connectives: the left division and a unary modality that occurs only with negative polarity and allows weakening in antecedents of sequents. We define the notion of a proof net for this calculus, which is similar to those for the ordinary Lambek calculus and multiplicative linear logic. We prove that a sequent is derivable in the calculus under consideration if and only if there exists a proof net for it. We present a polynomial-time algorithm for deciding whether an arbitrary given sequent is derivable in this calculus.