1. F₁ = P &or R, F₂ = ¬ P &or Q.
   Resolvent: R &or Q.
2. F₁ = ¬ P &or Q &or R, F₂ = ¬ Q &or S.
   Resolvent: ¬ P &or R &or S.
3. F₁ = ¬ P &or Q, F₂ = ¬ P &or R.
   Resolution not possible: no complementary literals.
4. F₁ = ¬ P &or Q &or S, F₂ = P &or ¬ Q &or R.
   Resolution not useful: two complementary literals.

Example of a proof by resolution:
Show that Q is a logical consequence of P &and (P &rarr Q).

1.	P	premise
2.	¬ P &or Q	premise
3.	¬ Q	negated conclusion
4.	Q	from 1 and 2
5.	□	from 3 and 4: Q.E.D.

Contents    Page-10    Prev    Next    Page+10    Index