A polynomial time algorithm for the Lambek calculus with brackets of bounded order
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Reconciling Lambek's restriction, cut-elimination, and substitution in the presence of exponential modalities
The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called "Lambek's restriction," that is, the antecedent o…
Extended Lambek calculi and first-order linear logic
First-order multiplicative intuitionistic linear logic (MILL1) can be seen as an extension of the Lambek calculus. In addition to the fragment of MILL1 which corresponds to the Lambek calculus (of Moot & Piazza 2001), I …
Comparing and evaluating extended Lambek calculi
Lambeks Syntactic Calculus, commonly referred to as the Lambek calculus, was innovative in many ways, notably as a precursor of linear logic. But it also showed that we could treat our grammatical framework as a logic (a…
The Logic for a Mildly Context-Sensitive Fragment of the Lambek-Grishin Calculus
While context-free grammars are characterized by a simple proof-theoretic grammatical formalism namely categorial grammar and its logic the Lambek calculus, no such characterizations were known for tree-adjoining grammar…
Vector Space Semantics for Lambek Calculus with Soft Subexponentials
We develop a vector space semantics for Lambek Calculus with Soft Subexponentials, apply the calculus to construct compositional vector interpretations for parasitic gap noun phrases and discourse units with anaphora and…
SentenceSentence Similarity