# Commutative operators in unification

Say I want to find a unification for the following two sentences in first-order logic:

1. P(x) & Q(y)
2. Q(A) & P(B)

Common sense tells us that {x: B, y: A} is such a unification. However, if I apply the standard unification algorithm, then we will go through the following steps:

1. Attempt to match & with & (succeeds, returns {}, go to step 2)
2. Attempt to unify P(x) with Q(A) (go to step 3)
3. Attempt to match P with Q (return failure)

The algorithm returns failure because it doesn't know that & is commutative.

We could fix that by telling our unification algorithm that And and Or are commutative. But more generally we might have a user-defined relation that is commutative, for example

1. IsRelated(Mother(x),Father(x))
2. IsRelated(Father(John),Mother(John))

Again, the standard unification algorithm would return failure, even though these terms can be unified.

How is this dealt with in practice, e.g. in theorem provers, or type inference algorithms?