The unification algorithm
Christopher John Hogger · 1990
Abstract There are many different species of algorithms available for computing most¬ general unifiers. The one most commonly employed in logic program interpreters is known as Robinson’s Algorithm (named after the discoverer of resolution).Its task is as follows. Given as input two atoms of the form in which the ri and ti are any terms, its aim is to decide whether the atoms are unifiable and-if they are-to deliver as output their most-general unifier; if they are not unifiable then the output is the message “failure”. In the initial set-up, all the term-pairs are stored on a stack S. Another stack 0, initially empty, is made available for accommodating those bindings (called ‘replacements’ in earlier Themes) which the algorithm will construct in the course of comparing each pair of terms on S. These two stacks are the only data structures required.