A polynomial time algorithm for the Lambek calculus with brackets of bounded order
This provides a computational solution for linguists and logicians working with extended categorial grammars, but it is incremental as it builds on prior work by Pentus.
The paper tackles the problem of determining provability in the Lambek calculus with brackets, a logical foundation for categorial grammar used in linguistics, by developing a polynomial-time algorithm that works when both formula depth and bracket nesting depth are bounded, combining tabularisation of proof nets with automata-theoretic methods.
Lambek calculus is a logical foundation of categorial grammar, a linguistic paradigm of grammar as logic and parsing as deduction. Pentus (2010) gave a polynomial-time algorithm for determ- ining provability of bounded depth formulas in the Lambek calculus with empty antecedents allowed. Pentus' algorithm is based on tabularisation of proof nets. Lambek calculus with brackets is a conservative extension of Lambek calculus with bracket modalities, suitable for the modeling of syntactical domains. In this paper we give an algorithm for provability the Lambek calculus with brackets allowing empty antecedents. Our algorithm runs in polynomial time when both the formula depth and the bracket nesting depth are bounded. It combines a Pentus-style tabularisation of proof nets with an automata-theoretic treatment of bracketing.