Horn formulas are a limited set of CNF expressions.


They are particularly useful in representing a set of operations and are the basis for the computer language PROLOG.  The limitation is that only one of the expressions in an inside parenthesis can be positive, but this is exactly what you might expect if you think about the following pattern:  if P gives us Q, and either Q or R gives us S, then we could rethink what we have as being that either P is false or Q is true and either Q is false or S is true at the same time that either R is false or S is true.

(P -> Q) & ((Q v R) -> S)

Imagine, for instance, that this describes a procedure in which you put a quarter in a machine.  If you Put in the quarter, then you now have a Quarter credit, and if you have either a Quarter credit or there is the Right change remaining you will get a Soda.

To get this into CNF we follow the same process as before.

(P -> Q) & ((Q v R) -> S)
(~P v Q) & (~(Q v R) v S)   MI
(~P v Q) & ((~Q & ~ R) v S)  DeM
(~P v Q) & (~Q v S) & (~R v S)   Dist

The point is that we can eliminate everything but S if in fact we have P or R as already true.  This is why only one letter in a parenthesis can be positive.