Using the algebra technique described in class:

Show that the following clauses

PvQ
~PvR
~QvR

logically entail the conclusion

R



PvQ = P+Q-PQ

~PvR = (1-P)+R-(1-P)R = 1-P + R - R + PR = 1-P+PR

~QvR = 1-Q+QR

~R or 1-R should give us a contradiction

"And" the clauses and the negation of the solution together:

(P+Q-PQ)(1-P+PR)(1-Q+QR)(1-R)


P   +PR  +Q  -PQ  +PQR
-P           -PQ  -PQR
             +PQ

PR +Q - PQ  = Q - PQ + PR


(Q-PQ+PR)(1-Q+QR)

Q   +QR  -PQ  -PQR +PR
-Q       +PQ  +PQR
              -PQR

PR + QR - PQR

(PR+QR-PQR)(1-R)

PR+QR-PQR
-PR-QR+PQR

0

Since I got zero, the premises necessarily entail the conclusion


I've never seen anyone use the algebra technique but me, but there is a very similar technique called "Proof by resolution" which is often implemented as an automatic theorem prover over propositional logic.

The problem with the algebra technique.  If I n variables, how many terms can I have in an algebraic logical expression?  Perhaps as many as 2^n.  (In actual practice, I tend not to, things tend to cancel, but they don't necessarily have to cancel, and I can have a very large of terms.

In the worst case, the algebraic method will run in exponential time, which is too bad, because if it did not, I have just proved that P=NP.

SATISFIABILITY is a known NP-complete problem.  If a logical expression is given in conjunctive normal form.  (CNF), SATISFIABILITY means can we find ANY assignment of variables (T or F) that will make the expression true.

CNF:

A disjunction is any group of variables (and negated) variables connected by v's.

Pv~QvRvS  <==disjunction

CNF is a bunch of disjunctions connected by conjunctions

(PvQ)^(Rv~S) is CNF.  Every logical can be put in conjunctive normal form.  You have the various distribution laws to do it.

~(PvQ) =   ~P^~Q  CNF

~(P^Q) ~Pv~Q  CNF

P^(QvR)  already in CNF

Pv(Q^R)  (PvQ)^(PvR)  <== CNF

Proof by resolution:

1.  Get all my clauses and my negated conclusion into CNF

(PvQ) (~PvR)  (~QvR)  ~R    <== They already are in CNF.

Find two clauses containing terms that negate each other.  Combine these two by removing the contradictory clauses and or-ing everything else together.  Add this new clause to the list.

(PvQ) (~PvR)  (~QvR)  ~R  (QvR) (PvR) ~P R ~Q Q P FALSE

If we make it all the way through trying all pairs of conjuncts, including new conjuncts without getting a FALSE, then the conclusion is NOT derivable from the propositions and if we ever get a FALSE anywhere in the process, then the conclusion is derivable from the propositions.

Given: P
Derive:  PvQ

P   ~(PvQ)

P  ~P^~Q

P ~P ~Q  FALSE


Algebra technique:  ~P ==> 1-P   (P^Q) = PQ  (PvQ) = 1-P+PQ   P^2 = P.

Proof by resolution:  Distributive laws, De Morgan's Laws, possibly commutative and associative laws.

There are also techniques in first order logic  (Ax)Px   (Ex)Px.  There are algorithms for automatic proving.  First order logic is both sound and complete.

Automated Theorem Prover:  Moebius's Four-Color Theorem.

Every planar graph can be colored in four colors so that no two adjacent nodes have the same color.  Finally proven in 1976, by two guys.  Kenneth Appel and Wolfgang Haken.  They broke it down into a very very large but finite number of cases, and then a computer colored those cases in four colors.