Paper: Normal Form Theorem Proving For The Lambek Calculus

ACL ID C90-2030
Title Normal Form Theorem Proving For The Lambek Calculus
Venue International Conference on Computational Linguistics
Session Main Conference
Year 1990

The possibility of multiple equivalent proofs presents a problem for efficient parsing of a number of flexible categorial grammar (CG) frameworks. In this paper I outline a normal form sys- tem for a sequent formulation of the product-free associative Lambek Calculus. This le,'~ls to a simple parsing approach that yields only normal form proofs. This approach is both ~afe in that all distinct readings for a sentence will be returned, and optimal in ~;hat there is only one normal form proof yielding each distinct meaning. 1 The Lambek Calculus The (product-free) Lambek Calculus (Lambek, 1958) is a highly flexible CG framework that can be given a sequent formulation with the following rules :23 (1) Axiom: x:f =~- x:/ Righ~ rules: F, y:i ~ x:f y:i, F ~ x:f F ----> x/y:Ai.f [/R]...