Solving generalized equations over infinite trees

In the paper a nondeterministic algorithm for solving sets of equations between terms built-up from individual constants and variables as well as functional constants and variables is given. It extends an algorithm for solving equations in the domain of infinite trees given by Colmerauer. Any solution computed by this algorithm is in a natural sense the smallest one and is semantically unique. The extension may be seen as a method of incorporating higher-order variables into logic programming languages.