CMPS140, Winter 2012, Section 01: Lecture 13

We are learning how to prove things in First Order Logic using resolution.

-1. Clausification is the process or converting FOL to clause form
and a recipe is given in the book.
0. Skolemization is the process of  removing existential quantifiers
(and replacing them with a constant or a function).
1. (we still need to cover resolution and unification).
EXAMPLE
   1.  prove:  A fool that knows he is a fool is no fool
     =>  No fools know they are fools...

       Ax [Fool(x) and Knowfool(x) => ~Fool(x)]
          =>
        ~Ey  [Fool(y) and Knowfool(y).]


      Clause form for hypothesis:
            ~Fool(x) or ~Knowfool(x) or ~Fool(x)
              which reduces to 1.  ~Fool(x) or ~Knowfool(x).
           Negated goal:
              Ey [Fool(y) and Knowfool(y)]
               which skolemized gives:
                   Fool(a) and Knowfool(a).

               which gives two clauses:
                    2. Fool(a)
                    3.  Knowlfool(a)

             Now 1,2 produce
                    4. ~Knowfool(a)
                  and 4,5 produce the empty clause.



   see http://www.cs.utexas.edu/~novak/reso.html
   for more examples and solutions.