A polynomial-time algorithm for the Lambek calculus with brackets of bounded order
Tipus de documentText en actes de congrés
Condicions d'accésAccés obert
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.
CitacióKanovich, M., Kuznetsov, S., Morrill, G., Scedrov, A. A polynomial-time algorithm for the Lambek calculus with brackets of bounded order. A: International Conference on Formal Structures for Computation and Deduction. "2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017: September 3-9, 2017, Oxford, UK". Oxford: Dagstuhl Publishing, 2017, p. 22.1-22.17.
Versió de l'editorhttp://drops.dagstuhl.de/opus/volltexte/2017/7738/