Đang chuẩn bị liên kết để tải về tài liệu:
Báo cáo khoa học: "CLASSICAL LOGICS FOR ATTRIBUTE-VALUE"

This paper describes a classical logic for attribute-value (or feature description) languages which ate used in urfification grammar to describe a certain kind of linguistic object commonly called attribute-value structure (or feature structure). Tile algorithm which is used for deciding satisfiability of a feature description is based on a restricted deductive closure construction for sets of literals (atomic formulas and negated atomic formulas). In contrast to the Kasper/Rounds approach (cf. [Kasper/Rounds 90]), we can handle cyclicity, without the need for the introduction of complexity norms, as in [Johnson 88J and [Beierle/Pletat 88]. . | CLASSICAL LOGICS FOR ATTRIBUTE-VALUE LANGUAGES Jiirgcn Wedekind Xerox Palo Alto Research Center and C.S.L.I. - Stanford University USA Abstract Thia paper describes a classical logic for attribute-value or feature description languages which are used in unification grammar to describe a certain kind of linguistic object commonly called attribute-value structure or feature structure . The algorithm which is used for deciding satisfiability of a feature description is based on a restricted deductive closure construction for sets of literals atomic formulas and negated atomic formulas . In contrast to the Kasper Rounds approach cf. Kasper Rounds 90 we can handle cyclicity without the need for the introduction of complexity norms as in Johnson 88 and Beierle Pletat 88 . The deductive closure construction is the direct proof-theoretic correlate of the congruence closure algorithm cf. Nelson Oppen 80 if it were used in attributevalue languages for testing satisfiability of finite sets of literals. I Introduction This paper describes a classical logic for attribute-value or feature description languages which arc used in unification grammar to describe a certain kind of linguistic object commonly called attribute-value structure or feature structure . From a logical point of view an attribute-value structure like e.g. the following in matrix notation PRED PROMISE TENSE PAST SUBJ q PREO JOHN SUIJJ CD XCOMP P ED ome can be regarded as a graphical representation of a minimal model of a satisfiable feature description. If we assume that the attributes in the example PRED TENSE SUBJ XCOMP are unary partial function symbols and the values a PROMISE PAST JOHN COME are constants then the given feature structure represents graphically e.g. the minimal model of the following description PRED SUBJa a JOHN fc TENSEa a PAST PREDa PROMISE SUBJa SUBJ XCOMPa PRED XCOMPa w COME .1 1 Note that the terms arc formed without using brackets. Since all function symbols are unary the .