Abstract

\ is a 7000 line Prolog parser/theorem-prover for logical categorial grammar. In such logical categorial grammar syntax is universal and grammar is reduced to logic: an expression is grammatical if and only if an associated logical statement is a theorem of a fixed calculus. Since the syntactic component is invariant, being the logic of the calculus, logical categorial grammar is purely lexicalist and a particular language model is defined by just a lexical dictionary. The foundational logic of continuity was established by Lambek while a corresponding extension including also logic of discontinuity was established by Morrill and Valentín :167–192, 2010). \ implements a logic including as primitive connectives the continuous and discontinuous connectives of the displacement calculus, additives, 1st order quantifiers, normal modalities, bracket modalities, and universal and existential subexponentials. In this paper we review the rules of inference for these primitive connectives and their linguistic applications, and we survey the principles of Andreoli’s focusing, and of a generalisation of van Benthem’s count-invariance, on the basis of which \ is implemented.