Another Resolution Example

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:

x[P(x) v Q(x)], x.¬P(x) x.Q(x)

1. Convert all premises to Clause Form:

   x[P(x) v Q(x)] ---> P(x) v Q(x) ---> [P(x), Q(x)] (where "--->" means "rewrites as")

   x.¬P(x) ---> [¬P(c)] (where c is a Skolem constant)

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

   ¬x.Q(x) ---> x.¬Q(x) ---> [¬Q(x)]

3. Union the above, renaming variables:

   {[P(x),Q(x)], [¬P(c)], [¬Q(y)]}

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}
                 \      /
                  \    /
                   \  /
                    \/
                    []