Prove using the resolution method that : $\varphi_1,\varphi_2,\varphi_3 \models \varphi_4 $ 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 :)
 A: 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.
