LP, the Larch Prover -- Matching
A term t1 is said to match a term t2 if it can be transformed
into t2 by some substitution of terms for
its variables. When operators with ac or commutative
operator theories occur in t1 and t2, or
when t1 and t2 contain quantifiers, t1
matches t2 in LP if there is a substitution that transforms t1 into a
term equivalent to t2 modulo these theories and changes of bound
variables.