Parallel Algorithms for Free and Associative-Commutative Unification

This 1990 work is written as a guide to the design of fast algorithms for free term matching, free unification and associative-commutative term matching. The goal of this research was to identify tractable unification problems, to evaluate existing methods for their solution and design new ones where appropriate. The emphasis is on speed, as measured by the worst-case complexity of algorithms. Only methods with direct relevance to practical use were chosen, and are presented in the wider context of unification theory. Few assumptions are made about the environment in which unification is to be used. Terms are represented as graphs, the most common data structure in use now. Results presented here should be useful in the implementation of fast symbolic manipulation systems and their application to scalable intelligent software.