Classical Logics for Attribute-Value Languages

CLASSICAL LOGICS FOR ATTRIBUTE-VALUE LANGUAGES J iirgen Wcdekind Xerox Palo Alto Research Center and C.S.L.I.- Stanford University USA Abstract This paper describes a classical logic for attribute-value (or fea- ture description) languages which ate used in urfification gram- mar to describe a certain kind of linguistic object commonly called attribute-value structure (or feature structure). Tile al- gorithm which is used for deciding satisfiability of a feature description is based on a restricted deductive closure construc- tion 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]. The deductive closure construction is the direct proof-theoretic correlate of the congruence closure algorithm (cf. [Nelson/Oppen 80]), if it were used in attribute- value languages for testing satisfiability of finite sets of literals. 1 Introduction This paper describes a classical logic for attribute-value (or fea- ture description) languages which are used in unification gram- mar to describe a certain kind of linguistic object commonly called attribute-value structure (or fcz~ture structure). From a logical point of view an attribute-vMue structure like e.g. tile following (in matrix notation) PRED 'PROMISE' TENSE PAST suBJ Pl :i) 'JOliN'] XCOMP [ SUBJ m ] PRED 'COME' can be regarded as a graphical representation of a mini- mal model of a satisfiable feature description. If we assume that the attributes (in the example: PRED, TENSE, SUB J, XCOMP) are unary partial function symbols and the values (a, 'PROMISE', PAST, 'JOIIN', 'COME') are constants then the given feature structure represents graphically e.g. the min- imal model of the following description: 'PRED SUBJa ~ 'JOIIN' &TENSEa ~, PAST & PREDa ~ 'PROMISE' & SUBJa ~ SUBJ XCOMPa & PRED XCOMPa ~ 'COME') I Note that the terms arc h)rnlcd without using brackets. (Since all function symbols are unary, the introduction of brackets would So, in the following attribute-value languages are regarded & quantifier-free sublanguages of classical first order language~ with equality whose (nonlogical) symbols are given by a set o" unary partial function symbols (attributes) and a set of con- stants (atomic and complex values). The logical vocabulary includes all propositional connectives; negation is interpreted (:lassically. 2 For quantifier-free attribute-value languages L we give an ax- iomatic or IIilbert type system ll°v which simply results from an ordinary first order system (with partial function symbols), if its language were restricted to the vocabulary of L. Accord- ing to requirements of tile applications, axioms for the constant- consistency, constant/complex-consistency and acyclicity can be added to force these properties for the feature structures (models). For deciding consistency (or satisfiability) of a feature descrip- tion, we assume .first, that the conjunction of the formulas ill,the feature dc'scription is converted to disjunctive normal form. Since a formula in disjunctive normal form is consis. tent, ill" at least one of its disjuncts is consistent, we only need all algorithm for.deciding consistency of finite sets of literals (atomic formulas …

Content truncated to 500 words