<<

. 87
( 107 .)



>>

course we have not yet proven the latter.) Remember that sentences whose main operator is a quanti¬er
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

<<

. 87
( 107 .)



>>