Commutative operators in unification

Question

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?

Answer 1

The keywords you want to look into are "AC Unification," "ACU Unification," and "Associative-commutative unification." People have been looking into this for a long time (see this 1987 paper, for example).