9f y[f ]x, we can define for trees x with only finitely many different subtrees (rational trees) the predicate x is a subtree of y" by

8z
?
y OE z ^ 8y1; y2 (y1 OE y2 OE z ! y1 OE z) ! x OE z
?

Here, the idea is to abuse" feature trees as sets, taking the direct subtrees of a tree as the elements of a set. Note that z fulfills the hypothesis in the above formula exactly if the set" z contains y and is transitive, and that hence the transitive closure of y is the smallest z which satisfies the hypothesis.

Thus, we can easily show (e.g., with the method of [30]) the undecidability of the theory of feature trees in the language of F. Consequently, in order to get a decidable sub-theory of F, we have to restrict the use of quantification over features.

The first contribution of this paper is the formulation of a decidable theory of feature trees which lies between CFT and F. The idea is to allow quantification over features only in order to state which features are defined, but not to quantify over the direct subtrees of a tree. More precisely, we will define the restricted theory of feature trees as the set of formulae where t in x[t]y is always a ground term, but where still atomic constraints xf# (f is defined on x"), where f may be a variable, are allowed. This situation is similar to Process Logic, where unrestricted quantification over path and state variables lead immediately to an undecidable validity problem, while a syntactic restriction leads to decidable sub-logic [22].

This restricted theory still is an essential extension of the theory of CFT. It extends CFT, since we can encode an arity constraint xff1; : : : ; fng as 8f (xf# $ Wni=1 f ?= fi). Beyond the expressivity of CFT, we can make statements about the arities of trees, for instance we can say that the arity of x is contained in the arity of y by

8f (xf# ! yf#)

As another example, the following formula expresses that x has exactly 3 features:

9f1; f2; f3
?
f1 ?6 = f2 ^ f2 ?6 = f3 ^ f1 ?6 = f3 ^ 8g (xg# $ [g ?= f1 _ g ?= f2 _ g ?= f3])
?

From these examples, one gets the idea that the theory of sets of feature symbols is hidden in our restricted theory of feature trees. This leads to the second contribution of our approach, which we now explain in three steps.

The first step is to realize that, in order to decide the validity of first order sentences over feature trees, we can save some work if we employ an existing decision algorithm for the theory of finite sets over infinitely many constants. Since this theory is easily encoded in the theory WS1S, the weak second order monadic theory of one successor function, the existence of such an algorithm follows immediately from Buchis result on the decidability of WS1S [11]1.

1The reader shouldn't be confused by the fact that we are apparently mixing first and second order structures. A second order structure can always be considered as a two-sorted first order structure, with one sort for the elements, and another sort for the sets. Only in the context of classes of structures makes it really sense to distinguish first order from second order structures.