A Complete and Recursive Feature Theory

A COMPLETE AND RECURSIVE FEATURE THEORY* Rolf Backofen and Gert Smolka German Research Center for Artificial Intelligence (DFKI) W-6600 Saarbr/icken, Germany {backofen,smolka} @dfki.uni-sb.de Abstract Various feature descriptions are being employed in constrained-based grammar formalisms. The com- mon notational primitive of these descriptions are functional attributes called features. The descrip- tions considered in this paper are the possibly quan- tified first-order formulae obtained from a signature of features and sorts. We establish a complete first- order theory FT by means of three axiom schemes and construct three elementarily equivalent models. One of the models consists of so-called feature graphs, a data structure common in computational linguistics. The other two models consist of so-called feature trees, a record-like data structure generaliz- ing the trees corresponding to first-order terms. Our completeness proof exhibits a terminating simplification system deciding validity and satisfia- bility of possibly quantified feature descriptions. 1 Introduction Feature descriptions provide for the typically partial description of abstract objects by means of functional attributes called features. They originated in the late seventies with so-called unification grammars [14], a by now popular family of declarative grammar for- malisms for the description and processing of natu- ral language. More recently, the use of feature de- scriptions in logic programming has been advocated and studied [2, 3, 4, 17, 16]. Essentially, feature de- scriptions provide a logical version of records, a data structure found in many programming languages. Feature descriptions have been proposed in vari- ous forms with various formalizations [1, 13, 9, 15, 5, 10]. We will follow the logical approach pioneered by [15], which accommodates feature descriptions as standard first-order formulae interpreted in first- order structures. In this approach, a semantics for *We appreciate discussions with Joachim Niehren and Ralf Treinen who read a draft version of this paper. The research reported in this paper has been supported by the Bundesminister ffir Forschung und Technologie under contracts ITW 90002 0 (DISCO) and ITW 9105 (Hydra). For space limitations proofs are omitted; they can be found in the complete paper [6]. feature descriptions can be given by means of a fea- ture theory (i.e., a set of closed feature descriptions having at least one model). There are two comple- mentary ways of specifying a feature theory: either by explicitly constructing a standard model and tak- ing all sentences valid in it, or by stating axioms and proving their consistency. Both possibilities are exemplified in [15]: the feature graph algebra ~" is given as a standard model, and the class of feature algebras is obtained by means of an axiomatization. Both approaches to fixing a feature theory have their advantages. The construction of a standard model provides for a clear intuition and yields a com- plete feature theory (i.e., if ¢ is a closed feature de- scription, then either ¢ or -~¢ is valid). The presenta- tion of a recursively enumerable axiomatization has the advantage that we inherit from predicate logic a sound and complete deduction system for valid fea- ture descriptions. The ideal case …

Content truncated to 500 words