. 88
( 107 .)


the conditionals true and hence S true as well.

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.
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
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.


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


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
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
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
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
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
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 ˆ
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


. 88
( 107 .)