# General resolution in first order logic

Assuming you have a formula in first order logic like

$$(\forall_x p(x) \land \forall_x q(x)) \rightarrow \forall_x(p(x) \land q(x))$$ (which seems valid?)

Converting the formula to CNF:

$$(\neg p(x) \vee \neg q(y) \vee p(z)) \land (\neg p(x) \vee \neg q(y) \vee q(z))$$

I don't see how I can apply general resolution to get the empty clause in this case which puzzles me since I believe the formula is valid.

Let $$\varphi$$ be your original formula. $$\lnot \varphi \equiv \forall_x \forall_y \exists_z (px \land qy \land (\lnot pz \lor \lnot qz))$$ Skolemization replaces $$z$$ by a function symbol $$f(x,y)$$: $$\lnot \varphi \equiv_{SAT} \forall_x \forall_y (px \land qy \land (\lnot pfxy \lor \lnot qfxy))$$ The corresponding clause set: $$\{\{px\},\{qy\},\{\lnot pfxy, \lnot qfxy\}\}$$ From there it should be straight-forward to derive the empty clause:
• Apply renaming $$\nu_1 = \{x/x_1\}$$ to $$\{px\}$$, yielding $$\{px_1\}$$, then resolve $$\{p x_1 \}$$ with $$\{ \lnot pfxy, \lnot qfxy\}$$ by $$\sigma_1 = \{ x_1 / fxy\}$$, yielding $$\{\lnot q fxy\}$$
• Apply renaming $$\nu_2 = \{y / y_1\}$$ to $$\{qy\}$$, yielding $$\{qy_1\}$$, then resolve $$\{qy_1\}$$ with $$\{ \lnot qfxy \}$$ by $$\sigma_2 = \{y_1/fxy\}$$, yielding the empty clause $$\Box$$
In conclusion, we have shown by resolution that $$\lnot \varphi$$ is unsatisfiable. Therefore $$\varphi$$ is valid.