1 Notice that we have now given two incompatible de¬nitions of what it means for an

assignment to satisfy a set of literals: one where we de¬ned what it means for an assignment

to satisfy a set of sentences thought of as a theory, and one where we think of the set as a

resolution clause. It would be better if two di¬erent words were used. But they aren™t, so

the reader must rely on context to tell which use is intended.

Section 17.4

490 / Advanced Topics in Propositional Logic

that in order for an assignment h to satisfy the set {C1 , C2 }, h will have

to assign true to at least one of Cube(a), Cube(b), or BackOf(b,a). So let

C3 = {Cube(a), Cube(b), BackOf(b, a)} be an additional clause. Then the set

of clauses {C1 , C2 } and {C1 , C2 , C3 } are satis¬ed by exactly the same assign-

ments. The clause C3 is a resolvent of the ¬rst set of clauses.

For another example, let C1 , C2 , and C3 be the following three clauses:

C1 = {Home(max), Home(claire)}

C2 = {¬Home(claire)}

C3 = {¬Home(max)}

Notice that in order for an assignment to satisfy both C1 and C2 , you will

have to satisfy the clause

C4 = {Home(max)}

Thus we can throw this resolvent C4 into our set. But when we look at

{C1 , C2 , C3 , C4 }, it is obvious that this new set of clauses cannot be satis-

¬ed. C3 and C4 are in direct con¬‚ict. So the original set is not tt-satis¬able.

With these examples in mind, we now de¬ne what it means for one clause,

say R, to be a resolvent of two other clauses, say C1 and C2.

De¬nition A clause R is a resolvent of clauses C1 and C2 if there is an atomic

resolvent de¬ned

sentence in one of the clauses whose negation is in the other clause, and if R

is the set of all the other literals in either clause.

Here are some more examples. Assume A, B, C, and D are atomic. We use

as above for the empty clause.

{A, D} {¬A}

{D}

{A, ¬A} {A}

{A}

{B, C} {¬B, ¬D}

{C, ¬D}

{D} {¬D}

The key fact about resolution is expressed in the following theorem. The

proof will be outlined in Exercise 17.45.

Chapter 17

Resolution / 491

Theorem (Completeness of resolution) If S is an not tt-satis¬able set of completeness of

resolution

clauses then it is always possible to arrive at by successive resolutions.

Here is an example which illustrates the resolution method. Suppose S is

the following sentence in CNF:

¬A § (B ∨ C ∨ B) § (¬C ∨ ¬D) § (A ∨ D) § (¬B ∨ ¬D)

Applying step 1, we convert the sentence S to a the following clauses:

{¬A}, {B, C}, {¬C, ¬D}, {A, D}, {¬B, ¬D}

Our new aim is to use resolution to show that this set of clauses (and hence

the original sentence S) is not tt-satis¬able.

Successive applications of step 2 is illustrated by the following picture:

{B, C} {¬C, ¬D}

{B, ¬D}

{A, D} {¬A} {¬B, ¬D}

{D} {¬D}

Since we are able to start with clauses in S and resolve to the empty clause,

we know that the original set T of sentences is not tt-satis¬able. A ¬gure of proof by resolution

this sort is sometimes called a proof by resolution.

A proof by resolution shows that a set of sentences, or set of clauses, is not

tt-satis¬able. But it can also be used to show that a sentence C is a tautological

consequence of premises P1 , . . . , Pn . This depends on the observation, made

earlier, that S is a consequence of premises P1 , . . . , Pn if and only if the set

{P1 , . . . , Pn , ¬S} is not tt-satis¬able.

Remember

1. Every set of propositional sentences can be expressed as a set of

clauses.

2. The resolution method is an important method for determining

whether a set of clauses is tt-satis¬able. The key notion is that of

a resolvent for a set of clauses.

3. A resolvent of clauses C1 and C2 is a clause R provided there is an

atomic sentence in one of the clauses whose negation is in the other

clause, and if R is the set of all the remaining literals in either clause.

Section 17.4

492 / Advanced Topics in Propositional Logic

Exercises

17.31 Open Alan Robinson™s Sentences. The sentences in this ¬le are not mutually satis¬able in any

‚| world. Indeed, the ¬rst six sentences are not mutually satis¬able. Show that the ¬rst ¬ve

sentences are mutually satis¬able by building a world in which they are all true. Submit this

as World 17.31. Go on to show that each sentence from 7 on can be obtained from earlier

sentences by resolution, if we think of the disjunction in clausal form. The last “sentence,” ,

is clearly not satis¬able, so this shows that the ¬rst six are not mutually satis¬able. Turn in

your resolution proof to your instructor.

17.32 Use Fitch to give an ordinary proof that the ¬rst six sentences of Alan Robinson™s Sentences are

‚ not satis¬able.

17.33 Construct a proof by resolution showing that the following CNF sentence is not satis¬able:

(A ∨ ¬C ∨ B) § ¬A § (C ∨ B ∨ A) § (A ∨ ¬B)

17.34 Construct a proof by resolution showing that the following sentence is not satis¬able. Since the

sentence is not in CNF, you will ¬rst have to convert it to CNF.

¬¬A § (¬A ∨ ((¬B ∨ C) § B)) § ¬C

17.35 Resolution can also be used to show that a sentence is logically true. To show that a sentence

is logically true, we need only show that its negation is not satis¬able. Use resolution to show

that the following sentence is logically true:

A ∨ (B § C) ∨ (¬A § ¬B) ∨ (¬A § B § ¬C)

Give resolution proofs of the following arguments. Remember, a resolution proof will demonstrate that

the premises and the negation of the conclusion form an unsatis¬able set.

17.36 17.37 17.38

¬B C∨A ¬A ∨ B

¬A ∨ C ¬C C ∨ ¬(A § B)

¬(C § ¬B)

A∨B ¬A ∨ (B § C)

¬A

17.39 17.40 17.41

A’B B’C A∨B

A A’C

(A § B) ’ C

B’D

B

C∨D

Chapter 17

Resolution / 493

17.42 17.43

A ∨ (B § C) ¬A ’ B

¬E C ’ (D ∨ E)

(A ∨ B) ’ (D ∨ E) D ’ ¬C

¬A A ’ ¬E

C§D C’B

17.44 (Soundness of resolution) Let S be a nonempty set of clauses.

1. Let C1 and C2 be clauses in S and let R be a resolvent of C1 and C2 . Show that S

and S ∪ {R} are satis¬ed by the same assignments.

2. Conclude that if S is satis¬able, then it is impossible to obtain by successive appli-

cations of resolution.

17.45 (Completeness of resolution) In this exercise we outline the theorem stated in the section to

the e¬ect that the resolution method is complete.

1. Assume that S is a set of clauses and that the only literals appearing in clauses are A

and ¬A. Show that if S is not satis¬able, then is a resolvent of clauses in S.

2. Next, assume that S is a set of clauses and that the only literals appearing in clauses

are A, B, ¬A, and ¬B. Form two new sets of clauses as follows. First, form sets S B and

S ¬B where the ¬rst of these consists of all clauses in S that do not contain B and

the second consists of all clauses in S that do not contain ¬B. Notice that these sets

can overlap, since some clauses in S might not contain either. Assume that S is not

satis¬able, and that h is any truth assignment. Show that if h(B) = true, then h

cannot satisfy S B . Similarly, show that if h(B) = false, then h fails to satisfy S ¬B .

3. With the same setup as above, we now form new sets of clauses SB and S¬B . The ¬rst

results from S B by throwing out ¬B from any clauses that contain it. The second results

from S ¬B by throwing out B from its clauses. Show that the observation made above

about h still holds for these new sets. Note, however, that neither B nor ¬B appears

in any clause in either of these sets. Hence, it follows that no assignment satis¬es SB

and that no assignment satis¬es S¬B.

4. Still continuing with the same setup, show that if S is not satis¬able, then can be

obtained as a resolvent of each of SB and S¬B . Here the result you obtained in part 1

comes into play.

5. Use this result to show that if S is not satis¬able then either or {¬B} can be

B

obtained as a resolvent from S . Show similarly that either or {B} can be obtained

as a resolvent from S ¬B.

6. Use this to show that if S is not satis¬able, then can be obtained as an eventual

resolvent of S.

Section 17.4

494 / Advanced Topics in Propositional Logic

7. Now you have shown that any unsatis¬able set S of clauses built from just two atomic

sentences has as an eventual resolvent. Can you see how this method generalizes to

the case of three atomic sentences? You will need to use your results for one and two

atomic sentences.

8. If you have studied the chapter on induction, complete this proof to obtain a general

proof of Theorem 17.4. Nothing new is involved except induction.

Chapter 17

Chapter 18

Advanced Topics in FOL

This chapter presents some more advanced topics in ¬rst-order logic. The ¬rst

three sections deal with a mathematical framework in which the semantics of

fol can be treated rigorously. This framework allows us to make our informal

notions of ¬rst-order validity and ¬rst-order consequence precise, and culmi-

nates in a proof of the Soundness Theorem for the full system F . The later

sections deal with uni¬cation and resolution resolution method, topics of im-

portance in computer science. The Completeness Theorem for F is taken up

in the next chapter, which does not presuppose the sections on uni¬cation

and resolution.

Section 18.1

First-order structures

In our treatment of propositional logic, we introduced the idea of logical con-

sequence in virtue of the meanings of the truth-functional connectives. We

developed the rigorous notion of tautological consequence as a precise approx-

imation of the intuitive notion. We achieved this precision thanks to truth ta-

ble techniques, which we later extended by means of truth assignments. Truth

assignments have two advantages over truth tables: First, in assigning truth

values to all atomic sentences at once, they thereby determine the truth or

falsity of every sentence in the language, which allows us to apply the concept

of tautological consequence to in¬nite sets of sentences. Second, they allow us

to do this with complete mathematical rigor.

In Chapter 10, we introduced another approximation of the intuitive notion

of consequence, that of ¬rst-order consequence, consequence in virtue of the

meanings of ∀, ∃ and =, in addition to the truth-functional connectives. We

described a vague technique for determining when a sentence was a ¬rst-order

consequence of others, but did not have an analog of truth tables that gave

us enough precision to prove results about this notion, such as the Soundness

Theorem for F.

Now that we have available some tools from set theory, we can solve this

problem. In this section, we de¬ne the notion of a ¬rst-order structure. A ¬rst- ¬rst-order structures

order structure is analogous to a truth assignment in propositional logic. It

495