Đang chuẩn bị liên kết để tải về tài liệu:
Báo cáo khoa học: "PARSING AS NATURAL DEDUCTION "

The logic behind parsers for categorial grammars can be formalized in several different ways. Lambek Calculus (LC) constitutes an example for a natural 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 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. . | Parsing as Natural Deduction Esther Kõnig . Universitât Stuttgart Institut fur 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 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 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 context-free grammars. Pereira Warren 1983 gave a characterization of these parsers as being resolution based theorem provers. Resolution might be taken as an instance of Hilbert-style theorem proving where there is one inference rule e.g. Modus Ponens or some other kind of Cut Rule which allows 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 combination 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 categorial grammars which make use of combination rules like