Case Study: Other Ways of Thinking - Thinking as Computation - page 259

That conditional says the same thing as the following disjunction:
not (

or p .
To see why, ask what it takes for the conditional to be false . This happens when q , r ,
and s are true, but p is false. Now what does it take for the disjunction to be false?
This happens when all the disjuncts are false, that is, when q , r , and s are true, but
p is false. So the conditional and the disjunction are equivalent : they are either both
false or both true. This means that the conditional “If q and r and s then p ” can also
be represented by a dclause: [p,not(q),not(r),not(s)] . (The order of the literals in
a dclause does not matter.)
In the example with Alice, Bob, and Carol, let the atoms a , b , and c stand for
the guilt of Alice, Bob, and Carol, respectively. Then the three given facts can be
represented as a CNF formula:
[ [a,b,c], [not(a),b], [a,not(c)] ]

) or not ( ) or not ( )

q r s

This gives the following:
The first dclause says that Alice is guilty or Bob is guilty or Carol is guilty (which
is just another way of saying that at least one of them is guilty).

The second dclause says that Alice is not guilty or Bob is guilty (which is an
equivalent way of saying that if Alice is guilty, then so is Bob).

The third dclause says that Alice is guilty or Carol is not guilty (which is an
equivalent way of saying that if Alice is not guilty, then neither is Carol).

So every conditional can be represented as a dclause (containing precisely one
unnegated literal), and once it is determined how to calculate logical entailments
for CNF formulas in general, that procedure will work for conditionals too.
Although every clause can be rewritten as a dclause, the converse is not true. For
example, there is no way to represent [not(p)] as a clause. Although there was a
form of negation in queries and in the bodies of clauses, there is no way to have a
simple negative fact (like Alice is not guilty ) in a Prolog knowledge base.

11.4.2 Satisfiability

How does logical entailment work for CNF formulas? So far, a collection of sentences
S 1 , S 2 , ..., S n logically entails a sentence S if S has to be true when the S i are all true.
Another way of saying this is that the sentences cannot all be

true. A set of sentences is said to be satisfiable if they can all be true, and unsatisfiable
otherwise. So to compute if a collection of sentences S i entails another S , it is sufficient

{ S 1 , S 2 , ... , S n , not ( S ) }