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

May 01, 2017 · The Ethereal · 🏛 International Conference on Formal Structures for Computation and Deduction

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Max Kanovich, Stepan Kuznetsov, Glyn Morrill, Andre Scedrov arXiv ID 1705.00694 Category cs.LO: Logic in CS Cross-listed cs.CL, cs.DS, cs.FL Citations 7 Venue International Conference on Formal Structures for Computation and Deduction Last Checked 5 months ago

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.