This time, let™s look at the sentence

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

Writing this in conditional form, we obtain

((A § B) ’ ⊥) § (B ’ C) § ( ’ B)

We won™t actually write out the table, but instead will just talk through the

method. First, we see that if the sentence is to be satis¬ed, we must assign

true to B, since ’ B is a conjunct. Then, looking at the second conjunct,

B ’ C, we see that assigning true to B forces us to assign true to C. But at

this point, we run out of things that we are forced to do. So we can assign A

the value false getting get an assignment that makes remaining conditional,

and hence the whole sentence, true.

How do we know that this algorithm is correct? Well, we don™t, yet. The

correctness of algorithm

examples may have convinced you, but they shouldn™t have. We really need

to give a proof.

Theorem The algorithm for the satis¬ability of Horn sentences is correct, in

that it classi¬es as tt-satis¬able exactly the tt-satis¬able Horn sentences.

Proof: There are two things to be proved here. One is that any

tt-satis¬able sentence is classi¬ed as tt-satis¬able by the algorithm.

The other is that anything classi¬ed by the algorithm as tt-satis¬able

really is tt-satis¬able. We are going to prove this result for the form

of the algorithm that deals with conditionals. Before getting down

to work, let™s rephrase the algorithm with a bit more precision. De-

¬ne sets T 0 , T 1 , . . . of atomic sentences, together with and ⊥, as

follows. Let T 0 = { }. Let T n be the set consisting of together

Chapter 17

Horn sentences / 485

with all atomic sentences A such that ’ A is a conjunct of S. More

generally, given T n , de¬ne T n+1 to be T n together with all atomic

sentences A such that for some B1 , . . . , Bk in T n , (B1 § . . . § Bk ) ’ A

is a conjunct of S. Notice that T n ⊆ T n+1 for each n. Since there are

only ¬nitely many atomic sentences in S, eventually we must have

T N = T N+1 . The algorithm declares S to be tt-satis¬able if and only

if ⊥ ∈ T N . Furthermore, it claims that if ⊥ is not in T N , then we

can get a truth assignment for S be assigning true to each atomic

sentence in T N and assigning false to the rest.

To prove the ¬rst half of correctness, we will show that if S is tt-

satis¬able, then ⊥ ∈ T N . Let h be any truth assignment that makes

S true. An easy proof by induction on n shows that h(A) = true for

each A ∈ T n . Hence ⊥ ∈ T N , since h(⊥) = false.

To prove the other half of correctness, we suppose that ⊥ ∈ T N

and de¬ne an assignment h by letting h(A) = true for A ∈ T N ,

and letting h(A) = false for the other atomic sentences of S. We

need to show that ˆ h(S) = true. To do this, it su¬ces to show that

ˆ

h(C) = true for each conditional C that is a conjunct of S. There

are three types of conditionals to consider:

Case 1: The conjunct is of the form ’ A. In this case A is in T 1.

But then ˆ assigns true to the A and so to the conditional.

h

Case 2: The conjunct is of the form (A1 §. . . §An ) ’ B. If each of the

Ai gets assigned true, then each is in T N and so B is in T N+1 = T N .

But then ˆ assigns true to B and so to the conditional. On the other

h

hand, if one of the Ai gets assigned false then the conditional comes

out true under ˆ h.

Case 3: The conjunct is of the form (A1 §. . . §An ) ’ ⊥. Since we are

assuming ⊥ ∈ T N , at least one of Ai is not T N , so it gets assigned

false by h. But then the antecedent of conditional comes out false

under ˆ so the whole conditional come out true.

h

Remember

1. A Horn sentence is a propositional sentence in CNF such that every

disjunction of literals in contains at most one positive literal.

2. The satisfaction algorithm for Horn sentences gives an e¬cient algo-

rithm to tell whether a Horn sentence is tt-satis¬able.

Section 17.3

486 / Advanced Topics in Propositional Logic

Exercises

17.17 If you skipped the You try it section, go back and do it now. Submit the ¬le Table Horn 1.

‚

17.18 A sentence in CNF can be thought of as a list of sentences, each of which is a disjunction of

‚ literals. In the case of Horn sentences, each of these disjunctions contains at most one positive

literal. Open Horn™s Sentences. You will see that this is a list of sentences, each of which is a

disjunction of literals, at most one of which is positive. Use the algorithm given above to build

a world where all the sentences come out true, and save it as World 17.18.

17.19 Open Horn™s Other Sentences. You will see that this is a list of sentences, each of which is a

‚ disjunctive Horn sentence. Use the algorithm given above to see if you can build a world where

all the sentences come out true. If you can, save the world as World 17.19. If you cannot, explain

how the algorithm shows this.

17.20 Rewrite the following Horn sentences in conditional form. Here, as usual, A, B, and C are taken

to be atomic sentences.

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

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

3. (¬A ∨ B) § (A ∨ ¬B)

Use Boole to try out the satisfaction algorithm on the following Horn sentences (two are in conditional

form). Give the complete row that results from the application of the algorithm. In other words, the table

you submit should have a single row corresponding to the assignment that results from the application

of the algorithm. Assume that A, B, C, and D are atomic sentences. (If you use Verify Table to check

your table, Boole will tell you that there aren™t enough rows. Simply ignore the complaint.)

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

‚ ‚

17.23 A § (¬A ∨ B) § ¬B 17.24 ¬A § (¬A ∨ B) § ¬B

‚ ‚

17.25 ((A § B) ’ C) § (A ’ B) § A § ((C § B) ’ D)

‚

17.26 ((A § B) ’ C) § (A ’ B) § A § ((C § B) ’ ⊥)

‚

Chapter 17

Horn sentences / 487

The programming language Prolog is based on Horn sentences. It uses a slightly di¬erent notation,

though. The clause

(A1 § . . . § An ) ’ B

is frequently written

B : ’ A1 , . . . , An

or

B ← A1 , . . . , An

and read “B, if A1 through An .” The following exercises use this Prolog notation.

17.27 Consider the following Prolog “program.”

AncestorOf(a, b) ← MotherOf(a, b)

AncestorOf(b, c) ← MotherOf(b, c)

AncestorOf(a, b) ← Father(a, b)

AncestorOf(b, c) ← Father(b, c)

AncestorOf(a, c) ← AncestorOf(a, b), AncestorOf(b, c)

MotherOf(a, b) ← true

FatherOf(b, c) ← true

FatherOf(b, d) ← true

The ¬rst ¬ve clauses state instances of some general facts about the relations mother of, father

of, and ancestor of. (Prolog actually lets you say things with variables, so we would not actually

need multiple instances of the same scheme. For example, rather than state both the ¬rst two

clauses, we could just state AncestorOf(x, y) ← MotherOf(x, y).) The last two clauses describe

some particular facts about a, b, c, and d. Use the Horn satisfaction algorithm to determine

whether the following set of Horn sentences (in conditional form) is satis¬able.

17.28 The Prolog program in Exercise 17.27 might be considered as part of a database. To ask

whether it entails B, Prolog adds

⊥←B

to the database and runs the Horn algorithm on the enlarged database. If the algorithm fails,

then Prolog answers “yes.” Otherwise Prolog answers “no.” Justify this procedure.

17.29 Use the procedure of the Exercise 17.28 to determine whether the following are consequences

of the Prolog program given in Exercise 17.27.

1. Ancestor(a, c)

2. Ancestor(c, d)

3. Mother(a, b)

4. Mother(a, d)

Section 17.3

488 / Advanced Topics in Propositional Logic

17.30 Suppose you have a Horn sentence which can be put into conditional form in a way that does

not contain any conjunct of form 3 in Proposition 7. Show that it is satis¬able. Similarly, show

that if it can be put into a conditional form that does not contain a conjunct of form 2, then

it is satis¬able.

Section 17.4

Resolution

People are pretty good at ¬guring out when one sentence is a tautological

consequence of another, and when it isn™t. If it is, we can usually come up

with a proof, especially when we have been taught the important methods of

proof. And when it isn™t, we can usually come up with an assignment of truth

values that makes the premises true and the conclusion false. But for computer

applications, we need a reliable and e¬cient algorithm for determining when

one sentence is a tautological consequence of another sentence or a set of

sentences.

Recall that S is a tautological consequence of premises P1 , . . . , Pn if and

only if the set {P1 , . . . , Pn , ¬S}is not tt-satis¬able, that is to say, its conjunc-

tion is not tt-satis¬able. Thus, the problem of checking for tautological conse-

quence and the problem of checking to see that a sentence is not tt-satis¬able

amount to the same thing. The truth table method provides us with a reliable

method for doing this. The trouble is that it can be highly expensive in terms

of time and paper (or computer memory). If we had used it in Fitch, there

are many problems that would have bogged down your computer intolerably.

In the case of Horn sentences, we have seen a much more e¬cient method,

one that accounts for the importance of Horn sentences in logic programming.

In this section, we present a method that applies to arbitrary sentences in

CNF. It is not in general as e¬cient as the Horn sentence algorithm, but

it is often much more e¬cient than brute force checking of truth tables. It

also has the advantage that it extends to the full ¬rst-order language with

quanti¬ers. It is known as the resolution method, and lies at the heart of many

applications of logic in computer science. While it is not the algorithm that

we have actually implemented in Fitch, it is closely related to that algorithm.

The basic notion in resolution is that of a set of clauses. A clause is just

set of clauses

any ¬nite set of literals. Thus, for example,

C1 = {¬Small(a), Cube(a), BackOf(b, a)}

is a clause. So is

C2 = {Small(a), Cube(b)}

Chapter 17

Resolution / 489

The special notation is used for the empty clause. A clause C is said to empty clause

be satis¬ed by a truth assignment h provided at least one of the literals in

C is assigned true by ˆ 1 The empty clause clearly is not tt-satis¬able by

h.

any assignment, since it does not contain any elements to be made true. If

C = then h satis¬es C if and only if the disjunction of the sentences in C

is assigned true by ˆ

h.

A nonempty set S of clauses is said to be satis¬ed by the truth assignment

h provided each clause C in S is satis¬ed by h. Again, this is equivalent to

saying that the CNF sentence formed by conjoining the disjunctions formed

ˆ

from clauses in S is satis¬ed by h.

The goal of work on resolution is to come up with as e¬cient an algorithm

as possible for determining whether a set of clauses is tt-satis¬able. The basic

insight of the theory stems from the observation that in trying to show that

a particular set S is not tt-satis¬able, it is often easier to show that a larger

set S derived from it is not tt-satis¬able. As long as the method of getting

S from S insures that the two sets are satis¬ed by the same assignments, we

can work with the larger set S . Indeed, we might apply the same method

over and over until it became transparent that the sets in question are not

tt-satis¬able. The method of doing this is the so-called resolution method.

Resolution Method: resolution method

1. Start with a set T of sentences in CNF which you hope to show is not

tt-satis¬able. Transform each of these sentences into a set of clauses in

the natural way: replace disjunctions of literals by clauses made up of

the same literals, and replace conjunctions by sets of clauses. Call these

set of all these clauses S. The aim now is to show S is not tt-satis¬able.

2. To show S is not tt-satis¬able, systematically add clauses to the set in

such a way that the resulting set is satis¬ed by the same assignments

as the old set. The new clauses to throw in are called resolvents of old resolvents

clauses. If you can ¬nally get a set of clauses which contains , and

so obviously cannot be satis¬ed, then you know that our original set S

could not be satis¬ed.

To complete our explanation of the resolution method, we need to explain

the idea of a resolvent. To make this more understandable, we ¬rst give a