are treated as atomic in the de¬nition of tautological consequence.

Chapter 17

Horn sentences / 479

17.9 17.10

∀x Dodec(x) ’ ∀x Large(x) ∀x (Dodec(x) ’ Large(x))

∀x Dodec(x) ∀x Dodec(x)

∀x Large(x) ∀x Large(x)

17.11 17.12

∀x Dodec(x) ’ ∀x Large(x) ∀x (Dodec(x) ’ Large(x))

∃x Dodec(x) ∃x Dodec(x)

∃x Large(x) ∃x Large(x)

17.13 Prove the half of Lemma 2 that we did not prove, the direction from right to left.

17.14 Prove the right-to-left half of Part (2) of 17.15 Prove the left-to-right half of Part (2) of

Lemma 3. Lemma 3.

17.16 In the inductive proof of Proposition 4, carry out the step for sentences of the form R ’ S.

Section 17.3

Horn sentences

In Chapter 4 you learned how to take any sentence built up without quanti¬ers

and transform it into one in conjunctive normal form (CNF), CNF, that is, one

which is a conjunction of one or more sentences, each of which is a disjunction

of one or more literals. Literals are atomic sentences and their negations. We

will call a literal positive or negative depending on whether it is an atomic positive and

negative literals

sentence or the negation of an atomic sentence, respectively.

A particular kind of CNF sentence turns out to be important in computer

science. These are the so-called “Horn” sentences, named not after their shape,

but after the American logician Alfred Horn, who ¬rst isolated them and stud-

ied some of their properties. A Horn Sentence is a sentence in CNF that has Horn sentences

the following additional property: every disjunction of literals in the sentence

contains at most one positive literal. Later in the section we will ¬nd that

there is a more intuitive way of writing Horn sentences if we use the connec-

tive ’. But for now we restrict attention to sentences involving only §, ∨,

and ¬.

The following sentences are all in CNF but none of them are Horn sen-

tences:

Section 17.3

480 / Advanced Topics in Propositional Logic

¬Home(claire) § (Home(max) ∨ Happy(carl))

(Home(claire) ∨ Home(max) ∨ ¬Happy(claire)) § ¬Happy(carl)

Home(claire) ∨ Home(max) ∨ ¬Home(carl)

The ¬rst sentence fails to be a Horn sentence because the second conjunct

contains two positive literals, Home(max) and Happy(carl). The second fails to

be a Horn sentence because of the ¬rst conjunct. It contains the two positive

literals Home(claire) and Home(max). Why does the third fail to be a Horn

sentence?

By contrast, the following are Horn sentences:

¬Home(claire) § (¬Home(max) ∨ Happy(carl))

Home(claire) § Home(max) § ¬Home(carl)

Home(claire) ∨ ¬Home(max) ∨ ¬Home(carl)

Home(claire) § Home(max) § (¬Home(max) ∨ ¬Home(max))

Examination of each shows that each conjunct contains at most one positive

literal as a disjunct. Verify this for yourself to make sure you understand

the de¬nition. (Remember that the de¬nition of CNF allows some degenerate

cases, as we stressed in Chapter 4.)

The de¬nition of Horn sentences may seem a bit ad hoc. Why is this

particular type of CNF sentence singled out as special? Using the material

conditional form of

Horn sentences conditional, we can put them in a form that is more intuitive. Consider the

following sentence:

(Home(claire) § Home(max)) ’ Happy(carl)

If we replace ’ by its equivalent in terms of ¬ and ∨, and then use DeMorgan™s

Law, we obtain the following equivalent form:

¬Home(claire) ∨ ¬Home(max) ∨ Happy(carl)

This is a disjunction of literals, with only one positive literal. Horn sentences

are just conjunctions of sentences of this sort.

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

sentences. If we replace ’ by its de¬nition, and use DeMorgan™s laws, we ¬nd

that each sentence on the left is logically equivalent to the Horn sentence on

the right.

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

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

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

The “typical” Horn sentence consists of a conjunction of sentences, each

of which is a disjunction of several negative literals and one positive literal,

Chapter 17

Horn sentences / 481

say,

¬A1 ∨ . . . ∨ ¬An ∨ B

This can be rewritten using § and ’ as:

(A1 § . . . § An ) ’ B

This is the typical case, but there are the important limiting cases, dis-

junctions with a positive literal but no negative literals, and disjunctions with

some negative literals but no positive literal. By a logical sleight of hand,

though, we can in fact rewrite these in the same conditional form. The sleight

of hand is achieved by introducing a couple of rather odd atomic sentences,

and our old friend ⊥. The ¬rst of these is assumed to be always true. The

second, of course, is always false. Using these,

¬A1 ∨ . . . ∨ ¬An

can be rewritten as:

(A1 § . . . § An ) ’ ⊥

Similarly, we can rewrite the lone atomic sentence B as ’ B. We summarize

these observations by stating the following result.

Proposition 7. Any Horn sentence of propositional logic is logically equiv-

alent to a conjunction of conditional statements of the following three forms,

where the Ai and B stand for ordinary atomic sentences:

1. (A1 § . . . § An ) ’ B

2. (A1 § . . . § An ) ’ ⊥

3. ’B

Using the truth table method, we could program a computer to check to see

if a sentence is tt-satis¬able or not since the truth table method is completely ine¬ciency of

truth tables

mechanical. You can think of our Taut Con routine as doing something like

this, though actually it is more clever than this brute force method. In general,

though, any method of checking arbitrary formulas for tt-satis¬ability is quite

“expensive.” It consumes a lot of resources. For example, a sentence involving

50 atomic sentences has 250 rows in its truth table, a very big number. For

Horn sentences, however, we can in e¬ect restrict attention to a single row. It

is this fact that accounts for the importance of this class of sentences.

This e¬cient method for checking the satis¬ability of Horn sentences, satisfaction algorithm

for Horn sentences

known as the satisfaction algorithm for Horn sentences, is really quite simple.

Section 17.3

482 / Advanced Topics in Propositional Logic

We ¬rst describe the method, and then apply it to a couple of examples. The

idea behind the method is to build a one-row truth table by working back and

forth, using the conjuncts of the sentence to ¬gure out which atomic sentences

need to have true written beneath them. We will state the algorithm twice,

once for the Horn sentences in CNF form, but then also for the conditional

form.

Satisfaction algorithm for Horn sentences: Suppose we have a Horn

satisfaction algorithm

for Horn sentences sentence S built out of atomic sentences A1 , . . . , An . Here is an e¬cient

procedure for determining whether S is tt-satis¬able.

1. Start out as though you were going to build a truth table, by listing all

the atomic sentences in a row, followed by S. But do not write true or

false beneath any of them yet.

2. Check to see which if any of the atomic sentences are themselves con-

juncts of S. If so, write true in the reference column under these atomic

sentences.

3. If some of the atomic sentences are now assigned true, then use these to

¬ll in as much as you can of the right hand side of the table. For example,

if you have written true under A5 , then you will write false wherever

you ¬nd ¬A5 . This, in turn, may tell you to ¬ll in some more atomic

sentences with true. For example, if ¬A1 ∨ A3 ∨ ¬A5 is a conjunct of S,

and each of ¬A1 and ¬A5 have been assigned false, then write true

under A3 . Proceed in this way until you run out of things to do.

4. One of two things will happen. One possibility is that you will reach a

point where you are forced to assign false to one of the conjuncts of

S, and hence to S itself. In this case, the sentence is not tt-satis¬able.

But if this does not happen, then S is tt-satis¬able. For then you can

¬ll in all the remaining columns of atomic sentences with false. This

will give you a truth assignment that makes S come out true, as we will

prove below. (There may be other assignments that make S true; our

algorithm just generates one of them.)

Let™s apply this algorithm to an example.

You try it

................................................................

1. Consider the sentence

Home(claire) § ¬Home(max) § (Home(max) ∨ ¬Home(claire))

Chapter 17

Horn sentences / 483

To make this ¬t on the page, let™s abbreviate the two atomic sentences

Home(claire) and Home(max) by C and M, respectively. Open Boole and

create the following table (it will be easier if you choose By Row in the

Edit menu):

C M C § ¬M § (M ∨ ¬C)

2. The ¬rst step of the above method tells us to put true under any atomic

sentence that is a conjunct of S. In this case, this means we should put a

true under C. So enter a t under the reference column for C.

3. We now check to see how much of the right side of the table we can ¬ll in.

Using Boole, check which columns on the right hand side call on columns

that are already ¬lled in. There is only one, the one under ¬C. Fill it in

to obtain the following:

C M C § ¬M § (M ∨ ¬C)

t f

4. Looking at the last conjunct, we see that if the whole is to be true, we

must also assign true to M. So ¬ll this in to obtain

C M C § ¬M § (M ∨ ¬C)

t t f

5. But this means the second conjunct gets assigned false, so the whole

sentence comes out false.

C M C § ¬M § (M ∨ ¬C)

t t f f

Thus, the sentence is not tt-satis¬able.

6. Finish this row of your table and save the table as Table Horn 1.

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .Congratulations

Let™s restate the satisfaction algorithm for Horn sentences in conditional

form, since many people ¬nd it more intuitive, and then apply it to an example.

Satisfaction algorithm for Horn sentences in conditional form: Suppose algorithm for

conditional Horn

we have a Horn sentence S in conditional form, built out of atomic sentences

sentences

A1 , . . . , An , as well as and ⊥.

1. If there are any conjuncts of the form ’ Ai , write true in the refer-

ence column under each such Ai .

Section 17.3

484 / Advanced Topics in Propositional Logic

2. If one of the conjuncts is of the form (B1 § . . . § Bk ) ’ A where you

have assigned true to each of B1 , . . . , Bk , then assign true to A.

3. Repeat step 2 as often as possible.

4. Again, one of two things will happen. You may reach a point where you

are forced to assign false to one of a conditional of the form (B1 § . . . §

Bk ) ’ ⊥ because you have assigned true to each of the Bi . In this case

you must assign false to S, in which case S is not tt-satis¬able. If this

does not happen, then ¬ll in the remaining reference columns of atomic

sentences with false. This will give a truth assignment that makes all