TEACH WANG                                 Chris Mellish  January 1983

=== THEOREM PROVING: WANG'S ALGORITHM ================================

Wang's algorithm is a means of proving theorems in the Propositional
Calculus. An alternative method is to use truth tables, but this
generally involves considerably more computation. Here is the basic
algorithm (repeated from Raphael).

   1. Write the premises down separated by commas, followed by an arrow and
      then the theorem to be proved. Eg:

         p, ~q ^ r     -->  p ^ ~q

      The aim is now to progressively remove connectives from this (using the
      rules 2, 3, 4 below) until condition 5 or condition 6 is met.

   2. If one of the formulae separated by commas is the negation of a
      formula, drop the negation sign and move it to the other side of the
      arrow. Eg:

         p, ~(q ^ r)   --> p ^ r

      is changed to:

         p --> p ^ r, q ^ r

   3. If the principal connective of a formula on the left is ^ (and), or on
      the right of the arrow is v (or), replace the connective by a comma.
      Eg:

         p, p ^ q  --> r, s

      is changed to:

         p, p , q  --> r, s

      and

         p, q --> r v p

      is changed to:

         p, q --> r, p

   4. If the principal connective of a formula on the left is v (or), or on
      the right of the arrow is ^ (and), then produce two new lines, each
      with one of the two sub-formulae replacing the formula. Both of these
      must be proved in order to prove the original theorem. Eg:

         p v q, r, s  --> q v p

      is changed to the two lines:

         p, r, s --> q v p
         q, r, s --> q v p

      Each of these must be independently successfully dealt with in order
      that the proof of the original formula is successful.

   5. If the same formula ever appears on both sides of an arrow, the line is
      proved.

   6. If no connectives (~, ^ or v) remain in a line, and no proposition
      appears on both sides of the arrow, the line cannot be proved.

The Propositional Calculus is not a powerful enough representation language
for most AI tasks. For information about theorem proving in the Predicate
Calculus, see * RESOLUTION.

Exercise
--------

Try to work out for yourself just why this algorithm works. Write a program
to apply the algorithm to an arbitrary Propositional Calculus problem. You
will have to find a way of representing Propositional Calculus formulae. Note
that the algorithm assumes that the only logical connectives used are ~
(not), ^ (and) and v (or). If you want to use other connectives, such as ->
(implies), you will have to convert your formulae before you can run the
algorithm. Try your program on the following:

    If the Russians get ahead of the Americans in the arms race, they will
    take over the world. If the Russians announce that they are cutting their
    arms budget, Congress will cut the American arms budget. If the
    Americans cut their arms budget, but the Russians do not cut theirs, the
    Russians will get ahead of the Americans in the arms race. The Russians
    are devious and will announce that they have cut their arms budget
    in any case. Either the SALT talks will fail or the Russians will cut
    their arms budget.

    If the SALT talks fail, will the Russians take over the world?
    If the SALT talks don't fail, will the Russians take over the world?

References
----------

Lemmon, E.J. "Beginning Logic", Nelson, 1972.

Raphael, B. "The Thinking Computer", Freeman, 1976 (Chapter 4).