We prove, by introducing a new kind of sequent calculus, that the decision problem for the non-associative Lambek calculus with product belongs to PTIME. This solves an open prolem...
Appeared in: N.V. Murray, editor, Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX’99), Lecture Notes in Artificial Intelligence 1617, Springer, pages 2...