Say I want to find a unification for the following two sentences in first-order logic:
- P(x) & Q(y)
- 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:
- Attempt to match & with & (succeeds, returns
{}
, go to step 2) - Attempt to unify P(x) with Q(A) (go to step 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
- IsRelated(Mother(x),Father(x))
- 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?