<<

. 94
( 107 .)



>>

Similarly, any set T of terms, of whatever size, is said to be uni¬able if there
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:

<<

. 94
( 107 .)



>>