The Lambek calculus, an intuitionistic fragment of linear logic, has recently been rediscovered by linguists. Due to its built-in hypothetical reasoning mechanism, it allows for describing a certain range of those phenomena in natural language syntax which involve incomplete subphrases or moved constituents. Previously, it seemed unclear how to extent traditional parsing techniques in order to incorporate reasoning about incomplete phrases, without causing the undesired effect of derivational equivalences. It turned out that the Larabek calculus offers a framework to formulate equivalent but more implementation-oriented calculi where this problem does not occur. In this paper, such a theorem prover for the Lambek calculus, i.e. a parser for Lambek categorial grammars, is defined. Permutations of proof steps which would cause derivational equivalence in a purely sequential formulation do not play a role in a (pseudo-)parallel approach which is based on a lemma table or a ‘chart’. At the same time, other redundant proof search which would occur in backtracking approaches is avoided.

The logic behind parsers for categorial grammars can be formalized in several different ways. Lambek Calculus (LC) constitutes an example for a natural deduction1 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 Lambek 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.