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 :)

  • $\begingroup$ you need to $\land$ the four statements, not $\lor$! $\endgroup$ – Bram28 Jan 23 '17 at 0:50
  • $\begingroup$ $\models$ can be typeset using \models. $\endgroup$ – Alex Kruckman Jan 23 '17 at 1:08
  • $\begingroup$ @user3719857 Do you have the resolution algorithm? Can you describe it to us step by step, and show us where you get stuck? $\endgroup$ – Bram28 Jan 23 '17 at 1:24


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.