is a single substitution of terms for some or all of the variables that occur in

terms of T so that all the resulting terms are identical.

Notice that whether or not terms are uni¬able is a purely syntactic notion.

It has to do with terms, not with what they denote. The terms father(Max)

and father(father(x)) are not uni¬able, regardless of whether or not Max is

a father. On the other hand, the terms father(father(Max)) and father(y) are

uni¬able. Just substitute father(Max) in for the variable y. This means that

we can decide whether a pair of terms is uni¬able without any idea of what

the terms happen to stand for.

Section 18.6

518 / Advanced Topics in FOL

Let™s give a couple more examples of uni¬cation. Suppose we have a binary

function symbol f and two unary function symbols g and h. Here is an example

of three terms that are uni¬able. Can you ¬nd the substitution that does the

trick?

f(g(z), x), f(y, x), f(y, h(a))

If you said to substitute h(a) for the variable x and g(z) for y you were right.

All three terms are transformed into the term f(g(z), h(a)). Are there any

other substitutions that would work? Yes, there are. We could plug any term

in for z and get another substitution. The one we chose was the simplest in

that it was the most general. We could get any other from it by means of a

most general uni¬ers

substitution.

Here are some examples of pairs, some of which can, others of which can-

not, be uni¬ed. See if you can tell which are which before reading on.

g(x), h(y)

h(f(x, x)), h(y)

f(x, y), f(y, x)

g(g(x)), g(h(y))

g(x), g(h(z))

g(x), g(h(x))

Half of these go each way. The ones that are uni¬able are the second, third,

and ¬fth. The others are not uni¬able. The most general uni¬ers of the three

that are uni¬able are, in order:

—¦ Substitute f(x, x) for y

—¦ Substitute some other variable z for both x and y

—¦ Substitute h(z) for x

The ¬rst pair is not uni¬able because no matter what you do, one will always

start with g while the other starts with h. Similarly, the fourth pair is not

uni¬able because the ¬rst will always start with a pair of g™s, while the second

will always start with a g followed by an h. (The reason the last pair cannot

be uni¬ed is a tad more subtle. Do you see why?)

There is a very general procedure for checking when two (or more) terms

are uni¬able or not. It is known as the Uni¬cation Algorithm. We will not

Uni¬cation Algorithm

explain it in this book. But once you have done the following exercises, you

will basically understand how the algorithm works.

Chapter 18

Resolution, revisited / 519

Exercises

18.22 Which of the following terms are uni¬- 18.23 Which of the following terms are uni¬-

able with father(x) and which are not? able with f(x, g(x)) and which are not?

If they are, give the substitution. If they If they are, give the most general uni-

are not, then explain why not. ¬er. If they are not, then explain why

1. Max not. (Here, as usual, a and b are names,

2. father(Claire) not variables.)

3. mother(Max) 1. f(a, a)

4. father(mother(Claire)) 2. f(g(a), g(a))

5. father(mother(y)) 3. f(g(x), g(g(x)))

6. father(mother(x)) 4. h(f(a, g(a)))

5. f(f(a, b), g(f(a, b)))

18.24 Find a set of four terms which can si- 18.25 Show that there are an in¬nite number

multaneously be uni¬ed to obtain the of di¬erent substitutions that unify the

following term: following pair of terms. Find one that is

most general.

h(f(h(a), g(a)))

g(f(x, y)), g(f(h(y), g(z)))

18.26 How many substitutions are there that

unify the following pair?

g(f(x, x)), g(f(h(a), g(b)))

Section 18.7

Resolution, revisited

In this section we discuss in an informal way how the resolution method for

propositional logic can be extended to full ¬rst-order logic by combining the extending resolution

to fol

tools we have developed above.

The general situation is that you have some ¬rst-order premises P1 , . . . , Pn

and a potential conclusion Q. The question is whether Q is a ¬rst-order con-

sequence of P1 , . . . , Pn . This, as we have seen, is the same as asking if there

is no ¬rst-order structure which is a counterexample to the argument that

Q follows from P1, . . . , Pn . This in turn is the same as asking whether the

sentence

P1 § . . . § Pn § ¬Q

Section 18.7

520 / Advanced Topics in FOL

is not fo-satis¬able. So the general problem can be reduced to that of deter-

mining, of a ¬xed ¬nite sentence, say S, of fol, whether it is fo-satis¬able.

The resolution method discussed earlier gives a procedure for testing this

when the sentence S contains no quanti¬ers. But interesting sentences do

contain quanti¬ers. Surprisingly, there is a method for reducing the general

case to the case where there are no quanti¬ers.

An overview of this method goes as follows. First, we know that we can

always pull all quanti¬ers in a sentence S out in front by logically valid trans-

formations, and so we can assume S is in prenex form.

Call a sentence universal if it is in prenex form and all of the quanti¬ers

universal sentences

in it are universal quanti¬ers. That is, a universal sentence S is of the form

∀x1 . . . ∀xn P(x1 , . . . , xn )

For simplicity, let us suppose that there are just two quanti¬ers:

∀x ∀y P(x, y)

Let™s assume that P contains just two names, b and c, and, importantly, that

there are no function symbols in P.

We claim that S is fo-satis¬able if and only if the following set T of

quanti¬er-free sentences is fo-satis¬able:

T = {P(b, b), P(b, c), P(c, b), P(c, c)}

Note that we are not saying the two are equivalent. S obviously entails T , so

if S is fo-satis¬able so is T . T does not in general entail S, but it is the case

that if T is fo-satis¬able, so is S. The reason is fairly obvious. If you have a

structure that makes T true, look at the substructure that just consists of b

and c and the relationships they inherit. This little structure with only two

objects makes S true.

This neat little observation allows us to reduce the question of the un-

reducing to

non-quanti¬ed satis¬ability of the universal sentence S to a sentence of fol containing no

sentences quanti¬ers, something we know how to solve using the resolution method for

propositional logic.

There are a couple of caveats, though. First, since the resolution method

caveats

for propositional logic gives us truth-assignments, in order for our proof to

work must be able to go from a truth-assignment h for the atomic sentences

of our language to a ¬rst-order structure Mh for that language making the

same atomic sentences true. This works for sentences that do not contain =,

as we saw in Exercise 18.12, but not in general. This means that in order to

be sure our proof works, the sentence S cannot contain =.

Chapter 18

Resolution, revisited / 521

Exercise 18.12 also required that the sentence not contain any function

symbols. This is a real pity, since Skolemization gives us a method for taking Skolemizing

any prenex sentence S and ¬nding another one that is universal and fo-

satis¬able if and only if S is: just replace all the ∃™s one by one, left to right, by

function symbols. So if we could only generalize the above method to the case

where function symbols are allowed, we would have a general method. This is

where the Uni¬cation Algorithm comes to the rescue. The basic strategy of

resolution from propositional logic has to be strengthened a bit.

Resolution method for fol: Suppose we have sentences S, S , S , . . . and resolution method

for fol

want to show that they are not simultaneously fo-satis¬able. To do this using

resolution, we would carry out the following steps:

1. Put each sentence S into prenex form, say

∀x1 ∃y1 ∀x2 ∃y2 . . . P(x1, y1, x2, y2 , . . . )

We can always make them alternate in this way by introducing some

null quanti¬ers.

2. Skolemize each of the resulting sentences, say

∀x1 ∀x2 . . . P(x1, f1 (x1 ), x2, f2 (x1 , x2 ), . . . )

using di¬erent Skolem function symbols for di¬erent sentences.

3. Put each quanti¬er free matrix P into conjunctive normal form, say

P1 § P2 § . . . § Pn

where each Pi is a disjunction of literals.

4. Distribute the universal quanti¬ers in each sentence across the con-

junctions and drop the conjunction signs, ending with a set of sen-

tences of the form

∀x1 ∀x2 . . . Pi

5. Change the bound variables in each of the resulting sentences so that

no variable appears in two of them.

6. Turn each of the resulting sentences into a set of literals by dropping

the universal quanti¬ers and disjunction signs. In this way we end up

with a set of resolution clauses.

7. Use resolution and uni¬cation to resolve this set of clauses.

Rather than explain this in great detail, which would take us beyond the

scope of this book, let™s look at a few examples.

Section 18.7

522 / Advanced Topics in FOL

Example. Suppose you want to show that ∀x P(x, b) and ∀y ¬P(f(y), b) are

not jointly fo-satis¬able, that is, that their conjunction is not fo-satis¬able.

With this example, we can skip right to step 6, giving us two clauses, each

consisting of one literal. Since we can unify x and f(y), we see that these two

clauses resolve to .

Example. Suppose we are told that the following are both true:

∀x (P(x, b) ∨ Q(x))

∀y (¬P(f(y), b) ∨ Q(y))

and we want to derive the sentence,

∀y (Q(y) ∨ Q(f(y)))

To show that this sentence is a ¬rst-order consequence of the ¬rst two, we

need to show that those sentences together with the negation of this sentence

are not simultaneously fo-satis¬able. We begin by putting this negation into

prenex form:

∃y (¬Q(y) § ¬Q(f(y)))

We now want to Skolemize this sentence. Since the existential quanti¬er in

our sentence is not preceded by any universal quanti¬ers, to Skolemize this

sentence we replace the variable y by a 0-ary function symbol, that is, an

individual constant:

¬Q(c) § ¬Q(f(c)))

Dropping the conjunction gives us the following two sentences:

¬Q(c)

¬Q(f(c))

We now have four sentences to which we can apply step 6. This yields the

following four clauses:

1. {P(x, b), Q(x)}

2. {¬P(f(y), b), Q(y)}

3. {¬Q(c)}

4. {¬Q(f(c))}

Applying resolution to these shows that they are not fo-satis¬able. Here is a

step-by-step derivation of the empty clause.

Resolvent Resolved Clauses Substitution

5. {Q(y), Q(f(y))} 1, 2 f(y) for x

6. {Q(f(c))} 3, 5 c for y

7. 4, 6 none needed

Chapter 18

Resolution, revisited / 523

Example. Let™s look at one more example that shows the whole method at

work. Consider the two English sentences: