CSE 463/563, Spring 2005

Another Resolution Example

Last Update: 17 March 2005

Note: NEW or UPDATED material is highlighted


Here's another example of the use of Refutation + Resolution + Unification to show the validity of a first-order inference:

Show that the following inference is valid:

  1. Convert all premises to Clause Form:

  2. Convert the negation of the conclusion (for Refutation) to Clause Form:

  3. Union the above, renaming variables:

  4. Apply Resolution to derive [ ]. Where Unification is needed in order to do this, show the MGU.

         [P(x),Q(x)] -P(c)	-Q(y)
              \      /      /
               \    /      /
          {x/c} \  /      /
                 \/      /
                Q(c)    /
                  \    /
             {y/c} \  /
                    \/
                    []
    

    Alternatively:

       [P(x),Q(x)]  -Q(y)	 -P(c)
            \         /        /
             \       /        /
              \     /        /
         {y/x} \   /        /
                \ /        /
                P(x)      / {x/c}
                  \      /
                   \    /
                    \  /
                     \/
                     []
    



Copyright © 2005 by William J. Rapaport (rapaport@cse.buffalo.edu)
file: 563S05/resolution-eg-2005-03-17.html