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.