Predict Logic Exercise

Question

I have a question regarding Resolution and Substitution We are Given the following rules

∀x∀y(p(x,y)=>∃z q(x,y,z))
∃x∀y∀z(r(y,z) <=> q(x,y,z))
∀x∃y (¬p(x,y) => ∀z q(x,y,z))

The question is, Can we prove this Rule

∃w ∃x ∃y ∃z ( r(x,y) ∧ q(x,w,z))

and we have these choices

1.true
2.false
c.Sometimes
d.It depends on Skolem constants' values.

at the beginning I know I must start with

¬(∃w ∃x ∃y ∃z ( r(x,y) ∧ q(x,w,z)))

so it will become

∀w ∀x ∀y ∀z ¬(r(x,y) ∧ q(x,w,z))
∀w ∀x ∀y ∀z (¬r(x,y) V ¬q(x,w,z))
¬r(x,y) V ¬q(x,w,z)

and then I should convert the given rules into CNF so we will have the following rules

1-  ¬p(x,y) V q(x,y,f(x,y))
2-  ¬r(y1,z1) V q(C1,y1,z1)
3-  ¬q(C1,y2,z2) V r(y2,z2)
4-  p(x3,f(x3)) V q (x3,f(x3),z3)
5-  ¬r(x4,y4) V ¬q(x4,w4,z4)

the answer is true, but I cannot prove that I feel like I am stuck so what is the right way to solve this question and get the correct answer?

Answer 1

First, a small correction: make sure to use a new skolem function if needed. So, you should get:

\begin{array}{ll} 1- & \neg p(x,y) \lor q(x,y,f_2(x,y))\\ 2- & \neg r(y_1,z_1) \lor q(c_1,y_1,z_1)\\ 3- & \neg q(c_1,y_2,z_2) \lor r(y_2,z_2)\\ 4- & p(x_3,f_1(x_3)) \lor q(x_3,f_1(x_3),z_3)\\ 5- & \neg r(x_4,y_4) \lor \neg q(x_4,w_4,z_4)\\ \end{array} Continue with:

\begin{array}{llll} 6. & q(x,f_1(x),f_2(x,f_1(x))) & (1,4) & [x/x_3,f_1(x)/y,f_2(x,f_1(x))/z_3]\\ 7. & r(f_1(c_1),f_2(c_1,f_1(c_1))) & (3,6) & [c_1/x,f_1(c_1)/y_2, f_2(c_1,f_1(c_1))/z_2]\\ 8. & \neg r(x,y_4) & (5,6) & [x/x_4,f_1(x)/w_4,f_2(x,f_1(x))/z_4]\\ 9. & \bot & (7,8) & f_1(c_1)/x, f_2(c_1,f_1(c_1))/y_4]\\ \end{array}

Answer 2

My Answer would be:

1-  ¬p(x,y) V q(x,y,f1(x,y))
2-  ¬r(y1,z1) V q(C1,y1,z1)
3-  ¬q(C1,y2,z2) V r(y2,z2)
4-  p(x3,f2(x3)) V q (x3,f2(x3),z3)
5-  ¬r(x4,y4) V ¬q(x4,w4,z4)

from (1,4) :

q (x3,f2(x3),z3) V q(x3,f2(x3),f1(x,f2(x3))) [x3|x ,f2(x3)|y]

then if we substitute [f1(x,f2(x3))|z3] we get:

6- q (x3,f2(x3),f1(x,f2(x3)))
7- ¬p(C1,y2) V r(y2,f1(C1,y2)) (1,3) [C1|x,y2|y,f1(C1,y2)|z2]
8- ¬r(x3,y4) (5+6) [x3|x4,f2(x3)|w4,f1(x,f2(x3))|z4]
9- q(C1,f2(C1),z3) V r(f2(C1),f1(C1,f2(C1))) (7,4) [C1|x3,f2(C1)|y2]

then if we try (9,3):

r(f2(C1),z3)V r(f2(C1),f1(C1,f2(C1))) [f2(C1)|y2,z3|z2]

then we substitute f1(C1,f2(C1))|z3 so we get:

10- r(f2(C1),f1(C1,f2(C1)))

finally:

11-⊥ (10,8)