EXPTIME Decidability of Nonassociative Lambek Calculus with Classical Logic (BFNL)
A complexity result for substructural logic showing that combining full classical (Boolean) propositional logic with the Nonassociative Lambek Calculus - the system BFNL - keeps the consequence relation decidable in exponential time. This locates BFNL between plain NL (polynomial-time decidable) and NL with non-distributive classical connectives (undecidable), matching the EXPTIME bound already known for the distributive case, and is proved using residuated-groupoid models.
2501.00493
This NCL'24 proceedings paper studies the computational complexity of the consequence relation for extensions of the Nonassociative Lambek Calculus (NL), a substructural logic that drops the structur…