(From Quine, quoted by Smullyan p 57 - described as difficult...)

P_{1} |
(∀x ((Fx ∧ Gx) → Hx)) → (∃y (Fy ∧ ¬Gy)) |

P_{2} |
(∀u (Fu → Gu)) ∨ (∀v (Fv → Hv)) |

C | (∀s ((Fs ∧ Hs) → Gs)) → (∃t (Ft ∧ Gt ∧ ¬Ht)) |

Transcription of P_{1}:

hence

hence

We note that P_{1} is not yet actually in *clausal form*; however, it proves more
convenient, on this occasion, to keep it as it is. The transcription of P_{2} is:

hence

Π_{u} and Π_{v} can migrate to the outer space (up two levels), and
can then be discarded, leading to

Transcription of ¬C:

hence

hence

The combined expression P_{1}∧P_{2}∧¬C then resolves as:

We note that the 'resolution' between the second and third clauses
involves first the substitution {**x**/t}, then an
application of the CL-rule

A (A(B)) = AB ≥ B

(where A and B are any CL-expressions), and is therefore perfectly admissible in a proof of the claim that a CLS-expression is mark-equivalent - which is what we are doing here.

If desired, the proof can be done 'by the book' - i.e. using clausal resolution. The first thing
is to convert the premise P_{1} into clausal form, which can be done by
using the CL-rule

repeatedly. Thus P_{1} is transformed as follows:

Now combine with

(Ft Gt (Ht))

and 'breed'. It is left as an exercise for the reader to obtain the clauses F_{y}
and (G_{y}) by this means. (Answer here.)

(From Robinson's 1963 paper, 'Theorem-proving on the computer', J. ACM 10 (Apr 1963), 163-174.) This is an example where we get serious about unification!

This example is taken from the field of Abstract Algebra. Suppose A is an algebra with a binary operation •. Thus, given any two elements x and y, they may be combined using • to produce a third element z; a situation which we symbolize by the equation

x•y = z.

Suppose further that • has the associative property, that is, for any three elements x, y and z,

(x•y)•z = x•(y•z);

and also, given two elements x and y, there are elements a and b satisfying the following equations:

a•x = y

x•b = y .

Show that the algebra has a left-inverse: that is, an element e such that

e•x = x

holds for every element x.

We first symbolize the known facts about A, and the statement that is to be proved, by formulae of first order logic.

The existence of • we represent as follows:

P_{1} |
∀x ∀y ∃z Qxyz |

Here the predication Qxyz means 'z is the result of combining x and y using •'. One way of representing the property of associativity would be to introduce a second two-place predicate meaning 'equals'; but there is another way of doing it. We make the statement:

P_{2} |
∀x ∀y ∀z ∀u ∀v ∀w (Qxyu∧Qyzv) → (Qxvw ↔ Quzw) |

In words: if u is x•y, and v is y•z, then w is x•v iff w is u•z. The remaining premises are:

P_{3} |
∀x ∀y ∃a Qaxy |

P_{4} |
∀x ∀y ∃b Qxby |

The statement to be proved is

C | ∃e ∀x Qexx |

When we transcribe into Laws of Form notation, P_{2} (associativity) may be split into two clauses:

P_{1}, P_{3}, P_{4} and ¬C become simply

For the proof by resolution, we need only the first clause of P_{2}, and do not need P_{1};
we also use P_{4} twice. The resolution-scheme
is:

(click on the diagram to bring up a magnified version). This is heavily dependent on unification - perhaps a more detailed explanation is in order? The first resolution step involves unification (one-making) of the terms

Q_{xvw}, Q_{exexe} .

This is achieved by the substitution

{ e/x , **x**_{e}/v , **x**_{e}/w } .

Remember, the substitution acts on the whole of both expressions which are participating in the resolution step, so all occurrences of x, v and w are replaced by the specified terms. The second step involves unification of

Q_{eyu}, Q_{akmkm},

achieved by means of

{ y/k , u/m , **a**_{yu}/e }.

This is why the term **x**_{ayu} appears in the resolution product. Next, we unite

Q_{uzxayu}, Q_{nbnpp}

by means of

{ u/n , **x**_{ayu}/p , **b**_{uxayu}/z };

and finally we must unite

Q_{ybuxayuxayu},
Q_{ibijj}.

Acting on the two terms at first with the substitution { y/i , **x**_{ayu}/j }

they become

Q_{ybuxayuxayu},
Q_{ybyxayuxayu}.

All that is needed to achieve complete union is to follow up with the substitution

{ y/u }

(or vice versa); then the term in the circle can be uncopied, leaving the sought-for empty mark - our goal!
It is interesting that the 'automatic' resolution process finally arrives at the 'insight' that y must be set equal to u
- even though it leaves it to the last possible moment. Whereas a typical human approach to the problem
of deriving our conclusion C *starts* with the insight that if there is a left-identity **e**, then it must
coincide with a
solution of the equation

**e**•**x** = **x**, ...(1)

where **x** is some arbitrarily chosen element of A. (The equation must have a solution by premise P_{3}.)
A 'human-style' proof might continue as follows:

Let c be any element of A; then, by P_{4}, there exists a element b such that

**x**•b = c . ...(2)

Then **e**•c = **e**•(**x**•b) (by (2))

= (**e**•**x**)•b (by P_{2})

= **x**•b (by(1))

= c (by(2)).

But c was any element of A; we may therefore conclude:

∀c **e**•c = c,

a statement which verifies our original claim C ◊

Let's see how our 'human' proof could be formalized in the language of the CLS-calculus. Let **x** be
a fixed element of A. We first note that

Q_{aijij} » Q_{axxxx}

(the left-hand expression reprents the premise P_{3}). Secondly, flowing
from P_{4}

Q_{fbfgg} » Q_{xbxcc}

Next, bringing in the first clause of P_{2}, and repeating the consequence of P_{4}
just derived:

Q_{axxxx} Q_{xbxcc}
Q_{xbxdd}
(Q_{xyu} Q_{yzv} Q_{uzw} (Q_{xvw}))

» Q_{xbxdd}
(Q_{xbxcw} (Q_{axxcw}))

» Q_{axxdd}

Thus our conclusion is 'implicated' in the premises. The skill lies in revealing that fact; it could be compared with the skill of the sculptor, who reveals the figure that is 'implicated' in the block of marble.

Our final example on this page is another example used by Robinson, again from the field of Abstract Algebra.
The problem is this. Let G be a group, with binary operation •, identity element **e**, and in which
every element x satisfies the equation

x•x = **e**

(so every element has order two). Prove that G is commutative, i.e. for every pair of elements a, b

a•b = b•a .

To tackle this, we first need to recall the group axioms. A group is a set G with • and **e**
such that

- • is associative: ∀x,y,z (x•y)•z= x•(y•z)
- every x satisfies
**e**•x = x•**e**= x - each x has an inverse y such that x•y = y•x =
**e**

In this problem, the third axiom is redundant, as each element is its own inverse. This leaves us with
five premises and a conclusion, as follows (P_{1} and P_{2} are the two halves
of the statement of associativity, as in Example 10.8):

P_{1} |
∀x ∀y ∀z ∀u ∀v ∀w (Rxyu∧Ryzv∧Ruzw) → Rxvw |

P_{2} |
∀x ∀y ∀z ∀u ∀v ∀w (Rxyu∧Ryzv∧Rxvw) → Ruzw |

P_{3} |
∀x Rxxe |

P_{4} |
∀x Rexx |

P_{5} |
∀x Rxex |

C | ∀a ∀b ∀c Rabc → Rbac |

¬C | ∃a ∃b ∃c Rabc ∧ ¬Rbac |

For the proof by resolution, we proceed in four stages:

We use P_{1}, P_{3} and P_{5}:

(The grey arrows indicate the terms that are united at each step. L_{1} is used as a
label for the second resolution product, as is L_{2} in the next stage.)

We use P_{2}, P_{3} and P_{4}:

This time we use the first half of ¬C, L_{1} (twice), and L_{2}. Note that when
L_{1} is applied to a term Rxyz it has the effect of swapping the 1st and 3rd indices; L_{2}
on the other hand swaps the 2nd and 3rd indices.

We bring in the second half of ¬C:

It is left as an exercise for the reader to translate the resolution-proof into a human-friendly form.