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...