
In both areas, first order predicate logic has been recognized as a powerful description language for feature trees. For the first area, this is immediate by the role of constraints in constraint logic programming [19] and in concurrent constrainedbased languages [26], while in the second area different approaches have been proposed. [24, 27, 20, 25] have advocated the use of predicate logic as feature description languages. [6] argues that predicate logic is the right language to express phenomena in both fields, and that feature trees constitute the canonical semantical model.
Feature trees [4] are possibly infinite, finitely branching trees, where the edges carry labels
taken from some given set of feature symbols. Features are functional, i.e., all edges departing
from the same node have different labels. In contrast to the usual definition from
the literature, we will omit
of nodes by socalled sort
der languages have been
sic class of predicate symany
first order feature lanrelation
symbols x[f ]y for
the standard model of feaof
this predicate is y is
der edge f". The feature
???
@
@
@
???
@
@
@
???
???
@
@
@
???
@
@
@
a c d c d
d c a
a b
Figure 1: A Feature Tree
in this paper the labeling
symbols. Different first orstudied.
The most babols,
which is contained in
guage, consists of binary
every feature symbol f . In
ture trees, the denotation
the direct subtree of x untheory
FT [4] is an axiomatization
of feature trees based exactly on this language (besides equality and sort predicates).
The feature theory CFT [28] uses a much more expressive language which extends
FT by socalled arity constraints xff1; : : : ; fng. The denotation of such a constraint in
the standard model is x has exactly edges labeled by f1; : : : ; fn departing from its root".
Furthermore, regular path expressions (which contain an implicit existential quantification
over feature paths, [7]), and subsumption ordering constraints [15, 14] have been considered.
Finally, the language F [31] contains a ternary feature predicate x[y]z. Using quantification
over features, all other feature theories can be embedded in the theory F [31, 6].
With the establishment of first order logic as feature description language, concrete problems concerning logical theories of feature trees have been attacked. After fixing an appropriate predicate logic language, these problems can be phrased as decision problems of certain, syntactically characterized fragments of the theory of feature trees. Satisfiability of existentially quantified conjunctions of atomic constraints (socalled basic constraints) and entailment between basic constraints is efficiently decidable for the languages FT [4] and CFT [28], and satisfiability of regular path constraints [7] and weak subsumption constraints [14] is decidable, while it is undecidable for subsumption constraints [13]. These considerations lead to the more general question whether the full first order theories of these languages is decidable. An affirmative answer was given for the case of FT [9] and CFT [10, 8]. Not surprisingly, the full first order theory of feature trees over F is undecidable, although the existential fragment of the theory is NPcomplete even with arity constraints as additional primitive notions [31].
The reason for the undecidability of F is the fact that it allows one to quantify over the direct subtrees of a tree. Taking x OE y (x is a direct subtree of y") as abbreviation of