Decidable Fragments of Calculi Used in CatLog

CatLog is a categorial grammar parser/theorem-prover developed by Glyn Morrill and his co-authors. CatLog is based on an extension of Lambek calculus. A distinctive feature of this extension is the usage of brackets for controlled non-associativity and a subexponential modality whose contraction rule interacts with bracketing in a sophisticated way. We consider two variants of the calculus, appearing in different versions of CatLog. Both systems are, unfortunately, undecidable in general. We consider fragments where the usage of subexponential is restricted by so-called bracket non-negative/non-positive conditions, prove that these fragments are decidable, and pinpoint their place in the complexity hierarchy. We also consider a more complicated, but more practically interesting problem of inducing (guessing) brackets. For this problem, we prove one decidability and one undecidability result, and leave some open questions for further research.