LP, the Larch Prover -- Unification

Two terms are unifiable if they have a common instance, i.e., if there is a substitution (called a unifier of the terms) that transforms them both into the same term. When two terms contain operators with ac or commutative operator theories, or when they contain quantifiers, they are unifiable if there is a substitution that transforms them into terms that are equivalent modulo these theories and changes of bound variables.

A set of unifiers for two terms is complete if every unifier of the two terms is a substitution instance of some unifier in the set. A unifier of two terms is a most general unifier if, whenever it is (equivalent to) a substitution instance of another unifier, that other unifier is also (equivalent to) a substitution instance of it. For any two unifiable terms containing ac and/or commutative operators, there is a finite set of most general unifiers that is complete.