<p>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 <a href="http://www.sciencedirect.com/science/article/pii/S0747717187800044">1987 paper, for example</a>). </p>

CC BY-SA 3.0
2012-07-25T00:51:05.480Z
2012-07-25T00:51:05.480Z
Rob Simmons
<p>Say I want to find a unification for the following two sentences in first-order logic:</p>

<ol>
<li>P(x) &amp; Q(y)</li>
<li>Q(A) &amp; P(B)</li>
</ol>

<p>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:</p>

<ol>
<li>Attempt to match &amp; with &amp; (<em>succeeds, returns <code>{}</code>, go to step 2</em>)</li>
<li>Attempt to unify P(x) with Q(A) (<em>go to step 3</em>)</li>
<li>Attempt to match P with Q (<em>return failure</em>)</li>
</ol>

<p>The algorithm returns failure because it doesn't know that &amp; is commutative.</p>

<p>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</p>

<ol>
<li>IsRelated(Mother(x),Father(x))</li>
<li>IsRelated(Father(John),Mother(John))</li>
</ol>

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

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

<ds.algorithms><lo.logic>
Commutative operators in unification
Chris Taylor
# Commutative operators in unification

(Asked by: username_0 on 2012-07-24)

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?

**Tags:** ds.algorithms, lo.logic

---

## 1 answers

### Answer by username_1 on 2012-07-25. Score: 9

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](http://www.sciencedirect.com/science/article/pii/S0747717187800044)).


---

