E-Unification: “Goal seeking” pattern matching between directed trees
This is called unification.  There is a one-to-one correspondence between terms and trees; the tree is the parse tree of a corresponding term.  It sounds like you want the most general unifier.  There are standard algorithms for solving this.  However, this doesn't handle equivalence relations like commutativity or associativity.  E-unification might be what you are looking for.