agum

The unification problem is given the problem statement t =? t', find a most general substitution s such that s(t) = s(t') modulo the axioms of an Abelian group. The matching problem is to find a most general substitution s such that s(t) = t' modulo the axioms. Substitition s is more general than s' if there is a substitition s" such that s' = s" o s.