How to Win a Game with Features

Rolf Backofen and Ralf Treinen

German Research Center for Artificial Intelligence (DFKI)
Stuhlsatzenhausweg 3
D-66123 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 Ehrenfeucht-Fra?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 well-established 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 so-called features, which are well-known 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