Unification (computer Science) - A Unification Algorithm

A Unification Algorithm

Given a unification problem consisting of a finite multi-set of potential equations on terms, the algorithm applies term rewriting rules to transform the multi-set of potential equations to an equivalent multi-set of equations of the form where are unique variables (appearing exactly once on the LHS of one equation, and nowhere else). A multi-set of this form can be read as a substitution. If there is no solution the algorithm terminates with . The set of variables in a term is written as, and the set of variables in all terms on LHS or RHS of potential equations in a problem is similarly written as . The operation of substituting all occurrences of variable in problem with term is denoted . For brevity constant symbols are regarded as function symbols having zero arguments.