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 determining provability of bounded depth formulas in L*, 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 in Lb*, 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.
@InProceedings{kanovich_et_al:LIPIcs.FSCD.2017.22, author = {Kanovich, Max and Kuznetsov, Stepan and Morrill, Glyn and Scedrov, Andre}, title = {{A Polynomial-Time Algorithm for the Lambek Calculus with Brackets of Bounded Order}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {22:1--22:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.22}, URN = {urn:nbn:de:0030-drops-77387}, doi = {10.4230/LIPIcs.FSCD.2017.22}, annote = {Keywords: Lambek calculus, proof nets, Lambek calculus with brackets, categorial grammar, polynomial algorithm} }
Feedback for Dagstuhl Publishing