# A polynomial time algorithm for the Lambek calculus with brackets of bounded order

## TL;DR

This paper presents a polynomial-time algorithm for the Lambek calculus with brackets, extending previous work to include brackets and empty antecedents, with efficiency guaranteed under bounded formula and bracket depths.

## Contribution

It introduces a novel polynomial-time algorithm for provability in the Lambek calculus with brackets, combining proof net tabularisation and automata-theoretic methods.

## Key findings

- Algorithm runs in polynomial time with bounded depths
- Extends previous algorithms to include brackets and empty antecedents
- Combines proof net tabularisation with automata theory

## Abstract

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.