Paper: Parsing As Natural Deduction

ACL ID P89-1033
Title Parsing As Natural Deduction
Venue Annual Meeting of the Association of Computational Linguistics
Session Main Conference
Year 1989

The logic behind parsers for categorial grammars can be formalized in several different ways. Lam- bek Calculus (LC) constitutes an example for a na- tural deduction 1 style parsing method. In natural language processing, the task of a parser usually consists in finding derivations for all different readings of a sentence. The original Lam- bek Calculus, when it is used as a parser/theorem prover, has the undesirable property of allowing for the derivation of more than one proof for a reading of a sentence, in the general case. In order to overcome this inconvenience and to turn Lambek Calculus into a reasonable parsing method, we show the existence of "relative" normal form proof trees and make use of their properties to constrain the proof procedure in the desired way.