2026-07-22T18:45:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:7738 2024-03-06T10:41:03Z ddc:004 open_access

A Polynomial-Time Algorithm for the Lambek Calculus with Brackets of Bounded Order Kanovich, Max Kuznetsov, Stepan Morrill, Glyn Scedrov, Andre Lambek calculus proof nets Lambek calculus with brackets categorial grammar polynomial algorithm 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Max Kanovich and Stepan Kuznetsov and Glyn Morrill and Andre Scedrov 2017 Is Part Of LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2017.22 urn:nbn:de:0030-drops-77387 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.22 eng https://creativecommons.org/licenses/by/3.0/legalcode