Nonassociative Lambek Calculus (NL) is a syntactic calculus of types introduced by Lambek [8]. The polynomial time decidability of NL was established by de Groote and Lamarche [4]. Buszkowski [3] showed that systems of NL with finitely many assumptions are decidable in polynomial time and generate context-free languages; actually the P-TIME complexity is established for the consequence relation of NL. Adapting the method of Buszkowski [3] we prove an analogous result for Nonassociative Lambek Calculus with unit (NL1). Moreover, we show (...) that any Lambek grammar based on NL1 (with assumptions) can be transformed into an equivalent context-free grammar in polynomial time. (shrink)

We discuss the logic of pregroups, introduced by Lambek [34], and its connections with other type logics and formal grammars. The paper contains some new ideas and results: the cut-elimination theorem and a normalization theorem for an extended system of this logic, its P-TIME decidability, its interpretation in L1, and a general construction of (preordered) bilinear algebras and pregroups whose universe is an arbitrary monoid.

A two-stage procedure is described which induces type-logical grammar lexicons from sentences annotated with skeletal terms of the simply typed lambda calculus. First, a generalized formulae-as-types correspondence is exploited to obtain all the type-logical proofs of the sample sentences from their lambda terms. The resulting lexicons are then optimally unified. The first stage constitutes the semantic bootstrapping (Pinker, Language Learnability and Language Development, Harvard University Press, 1984), while the unification procedure of Buszkowski and Penn represents a first attempt at structure-dependent (...) distributional learning of the syntactic and semantic categories. This effort extends earlier induction procedures (Buszkowski and Penn, 1990, Studia Logica 49, 431–454; Kanazawa, 1998, CSLI Publications and the European Association for Logic, Language and Information) for classical categorial grammar to at first the non-associative Lambek calculus, and then to a large class of type logics enriched by modal operators and structural rules. (shrink)

A two-stage procedure is described which induces type-logical grammar lexicons from sentences annotated with skeletal terms of the simply typed lambda calculus. First, a generalized formulae-as-types correspondence is exploited to obtain all the type-logical proofs of the sample sentences from their lambda terms. The resulting lexicons are then optimally unified. The first stage constitutes the semantic bootstrapping (Pinker, Language Learnability and Language Development, Harvard University Press, 1984), while the unification procedure of Buszkowski and Penn represents a first attempt at structure-dependent (...) distributional learning of the syntactic and semantic categories. This effort extends earlier induction procedures (Buszkowski and Penn, 1990, Studia Logica 49, 431–454; Kanazawa, 1998, CSLI Publications and the European Association for Logic, Language and Information) for classical categorial grammar to at first the non-associative Lambek calculus, and then to a large class of type logics enriched by modal operators and structural rules. (shrink)

A sequent calculus S for the variety tqBa of all topological quasi-Boolean algebras is established. Using a construction of syntactic finite algebraic model, the finite model property of S is shown, and thus the decidability of S is obtained. We also introduce two non-distributive variants of topological quasi-Boolean algebras. For the variety TDM5 of all topological De Morgan lattices with the axiom 5, we establish a sequent calculus S5 and prove that the cut elimination holds for it. Consequently the decidability (...) of S5 is established. Furthermore, this proof-theoretic method is applied to some subvarieties of TDM5. (shrink)