Parsing as Natural Deduction

PARSING AS NATURAL DEDUCTION Esther KSnig Universitgt Stuttgart Institut fiir Maschinelle Sprachverarbeitung, Keplerstrasse 17, D-7000 Stuttgart 1, FRG Abstract 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. 1 Introduction Sophisticated techniques have been developed for the implementation of parsers for (augmented) con- text-free grammars. [Pereira/Warren 1983] gave a characterization of these parsers as being resolu- tion based theorem provers. Resolution might be taken as an instance of Hilbert-style theorem pro- ving, where there is one inference rule (e.g. Modus Ponens or some other kind of Cul Rule) which al- lows for deriving theorems from a set of axioms. In the case of parsing, the grammar rules and the lexicon would be the axioms. When categorial grammars were discovered for computational linguistics, the most obvious way to design parsers for categorial grammars seemed 1 "natural deduction" is used here in its broad sense, i.e. natural deduction as opposed to Hilbert-style deduction to apply the existing methods: The few combi- nation rules and the lexicon constitute the set of axioms, from which theorems are derived by a resolution rule. However, this strategy leads to unsatisfactory results, in so far as extended ca- tegorial grammars, which make use of combina- tion rules like functional composition and type raising, provide for a proliferation of derivations for the same reading of a sentence. This pheno- menon has been dubbed the spurious ambiguity problem [Pareschi/Steedman 1987]. One solution to this problem is to describe normal forms for equivalent derivations and to use this knowledge to prune the search space of the parsing process [Hepple/Morrill 1989]. Other approaches to cope with the problem of spurious ambiguity take into account the peculari- ties of categorial grammars compared to grammars With "context-free skeleton". One characteristic of categorial grammars is the shift of information from the grammar rules into the lexicon: grammar rules are mere combination schemata whereas syntactic categories do not have to be atomic items as in the "context-free" formalisms, but can also be structu- red objects as well. The inference rule of a Hilbert-style deduction system does not refer to the internal structure of the propositions which it deals with. The alterna- tive to Hilbert-style deduction is natural deduction (in the broad sense of the word) which is "natural" in so far as at least some …

Content truncated to 500 words