A unification algorithm for infinite trees
Kuniaki Mukai · International Joint Conference on Artificial Intelligence · 1983
A simple unification algorithm for infinite trees has been developed. The algorithm designed to work efficiently under structure sharing implementations of logic programming languages, e.g., Prolog (Warren [3]). A relation, called is covered with, between two terms introduced to terminate the algorithm. The fundamental operations are to compute the frontier set of two given terms and to test the relation between them. A termination proof shown.