Feature Trees over Arbitrary Structures
Programming Systems Lab
German Research Center for Artificial Intelligence (DFKI)
Stuhlsatzenhausweg 3, D66123 Saarbrucken, Germany
This paper presents a family of first order feature tree theories, indexed by the theory of the feature labels used to build the trees. A given feature label theory, which is required to carry an appropriate notion of sets, is conservatively extended to a theory of feature trees with the predicates x[t]y (feature t leads from the root of tree x to the tree y), where we have to require t to be a ground term, and xt# (feature t is defined at the root of tree x). In the latter case, t might be a variable. Together with the notion of sets provided by the feature label theory, this yields a first-class status of arities.
We present a quantifier elimination procedure to reduce any sentence of the feature tree theory to an equivalent sentence of the feature label theory. Hence, if the feature label theory is decidable, the feature tree theory is too.
If the feature label theory is the theory of infinitely many constants and finite sets over infinitely many constants, we obtain an extension of the feature theory CFT, giving first-class status to arities. As an another application, we obtain decidability of the theory of feature trees, where the feature labels are words, and where the language includes the successor function on words, lexical comparison of words and first-class status of arities.
Feature trees have been introduced as record-like data structures in constraint (logic) programming , , and as models of feature descriptions in computational linguistics , . The use of record-like structures in logic programming languages, in the form of socalled -terms , was pioneered by the languages LOGIN  and LIFE . More recently, Oz [17, 26] uses a feature constraint system, the semantics of which is directly based on feature trees. In computational linguistics, feature structures have a long history in the field of unification grammars (as described in ).
?On leave to: L.R.I., B^at. 490, Universit?e Paris Sud, F91405 Orsay cedex, France, firstname.lastname@example.org
To appear in: Patrick Blackburn and Maarten de Rijke, eds., Logic, Structures and Syntax, Studies in Logic, Language and Information, 1995