
How to Win a Game with Features
Rolf Backofen and Ralf Treinen
German Research Center for Artificial Intelligence (DFKI)
Stuhlsatzenhausweg 3
D66123 Saarbrucken, Germany
email: fbackofen,[email protected]
Abstract. We show, that the axiomatization of rational trees in the language of features given elsewhere is complete. In contrast to other completeness proofs that have been given in this field, we employ the method of EhrenfeuchtFra?ss?e Games, which yields a much simpler proof. The result extends previous results on complete axiomatizations of rational trees in the language of constructor equations or in a weaker feature language.
1 Introduction
Rational trees are a canonical model for cyclic data structures or recursive type equations. The wellestablished language for trees in logic and computer science is the language Herbrand of constructor symbols, which provides for equations x = f(x1; : : : ; xn) as atomic formulae.
Here, we take a more elementary view. We use the language of socalled features, which are wellknown for a long time in computational linguistics and knowledge representation (see [12] for a survey). There are different possible choices of a feature language. A first language FT has been established in [3] and [1]. The language of FT consists of unary label predicates, which express that the root node of a tree has a certain label, and binary feature predicates, which serve as the partial selector functions for trees. For instance, we can translate a Herbrand formula x = f(x1; : : : ; xn) into feature logic as f(x) ^ 1(x; x1) ^ : : : ^ n(x; xn) or, in a more convenient syntax as fx ^ x1x1 ^ : : : ^ xnxn. In case of a finite signature ?, the predicates of feature logic can be defined in terms of Herbrand by taking an appropriate disjunction. In this case, 1(x; y) could be expressed as _
f2?
9?y x = f(y; ?y )
In case of infinitely many symbols, this is no longer possible, since for instance xfy is equivalent to an infinite disjunction in Herbrand.
There is a major gap between FT and Herbrand, since the translation into FT given above does not preserve validity of formulae. The problem is that a formula x = f(?x) has a unique solution in x when the ?x are given, but that the solution to x of the translated formula fx ^ x1x1 ^ : : : ^ xnxn is not unique, since x