Prove using the resolution method that : $\varphi_1,\varphi_2,\varphi_3 \models \varphi_4 $

Question

I have to prove using the resolution method that :

$\varphi_1,\varphi_2,\varphi_3 \models \varphi_4 $ where:

$\varphi_1 = \exists z\, \forall x\, ( \forall y\, (q(g(x),y) \vee p(z,g(x))) $

$\varphi_2 = \exists z\, \forall y\, ( p(y,g(g(y)) \rightarrow \forall x\, q(x, g(z))) $

$\varphi_3 = \forall x\, \forall y\, ( r(x, g(y)) \rightarrow (r(g(y),x) \vee \neg \exists x\, \exists y\, r(x,y))) $

$\varphi_4 = \exists z\, ( \exists x\, q(g(x), z) \wedge \exists x\, q(z,x)) $

I know that I have to use the method on $\varphi_1 \wedge \varphi_2 \wedge \varphi_3 \wedge \neg \varphi_4 $, but from there on I have no idea what to do. Any help is welcomed :)

Answer 1

Hint

See Resolution procedure :

(i) All sentences in the knowledge base and the negation of the sentence to be proved (the conjecture) are conjunctively connected.

(ii) The resulting sentence is transformed into a conjunctive normal form with the conjuncts viewed as elements in a set of clauses.

Consider e.g. the negated conclusion $\lnot \varphi_4$:

$¬ ∃z [ ∃x q(g(x),z) ∧ ∃xq(z,x) ]$.

It can be rewritten as :

$∀z ¬ [ ∃x q(g(x),z) ∧ ∃wq(z,w) ] \equiv ∀z [ ∀x ¬ q(g(x),z) ∨ ∀w ¬ q(z,w) ]$.

Then: (iii) convert it to Prenex normal form:

$∀z∀x∀w [ ¬ q(g(x),z) ∨ ¬ q(z,w) ]$,

and finally: (iv) Skolemize:

$¬ q(g(x),z) ∨ ¬ q(z,w)$.

This is one of the needed clauses.

Same for the four premise; for example, for $\varphi_1$ we have :

$q(g(x),y) ∨ p(c_1,g(x))$.

After completion of the preliminary work of transformation, we have to apply the resolution rule trying to derive the empty clause : $\square$.

---

Note. The empty clause (symbolized : $\square$ or $\{ \}$) is an empty disjunction and the convention is that an empty disjunction is always false. Thus, we may symbolize it also with: $\bot$ (the falsum).

The convention is justified by the fact that : $A \lor B \lor \bot \equiv A \lor B$, i.e. adding an empty disjunction to an existing disjunction does not alter its truth value.