ANOTHER RESOLUTION EXAMPLE

Show that the following inference is valid:

Ax[Px v Qx], Ex[-Px] |- Ex[Qx]

1. Convert all premises to Clause Form:

   Ax[Px v Qx] -> Px v Qx -> {PxQx}, where "->" means "rewrites as"

   Ex[-Px] -> {-Pc}, where c is a Skolem constant

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

   -Ex[Qx] -> Ax[-Qx] -> {-Qx}

3. Union the above, renaming variables:

   {PxQx, -Pc, -Qy}

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

   	PxQx	-Pc	Qy
             \      /      /
              \    /      /
         {c/x} \  /      /
                \/      /
                Qc     /
                 \    /
            {c/y} \  /
                   \/
                   {}       
   

   Alternatively:

   	PxQx    -Qy	-Pc
             \     /        /
        {x/y} \   /        /
               \ /        /
                Px       / {c/x}
                 \      /
                  \    /
                   \  /
                    \/
                    {}