<<

. 89
( 107 .)



>>

couple of examples. Let C1 and C2 be the clauses displayed earlier. Notice
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

<<

. 89
( 107 .)



>>