Unification and Anti-Unification Algorithms with Proximity Relations