ACL Anthology Network (All About NLP) (beta) The Association Of Computational Linguistics Anthology Network 
ACL ID  C902030 

Title  Normal Form Theorem Proving For The Lambek Calculus 
Venue  International Conference on Computational Linguistics 
Session  Main Conference 
Year  1990 
Authors 

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 productfree 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 (productfree) Lambek Calculus (Lambek, 1958) is a highly flexible CG framework that can be given a Gentzen..style 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]...