Resolution method (of first-order predicate logic) to show that the following formulas are unsatisfiable

Question

below is the problem I have and I able to get the clauses from the given formula.

Below are my steps.

EDIT

Formula

EDIT

¬((∀y.q(y))∨¬(∀x.(q(x)∨r(x))∧(∃z.¬p(z)∧(p(z)∨¬r(x)))))

(∃y.¬q(y))∧¬¬(∀x.(q(x)∨r(x))∧(∃z.¬p(z)∧(p(z)∨¬r(x))))

∃y(¬q(y)∧(∀x.(q(x)∨r(x))∧(∃z.¬p(z)∧(p(z)∨¬r(x)))))

∃y∀x(¬q(y)∧((q(x)∨r(x))∧(∃z.¬p(z)∧(p(z)∨¬r(x)))))

∃y∀x∃z(¬q(y)∧((q(x)∨r(x))∧(¬p(z)∧(p(z)∨¬r(x)))))

standarize variables

∀x∃z(¬q(c)∧((q(x)∨r(x))∧(¬p(z)∧(p(z)∨¬r(x)))))

∀x(¬q(c)∧((q(x)∨r(x))∧(¬p(f(x))∧(p(f(x))∨¬r(x)))))

So i got below cluases

1. {¬q(c)}
2. {q(x),r(x)}
3. {¬p(f(x)}
4. {p(f(x),¬r(x)}
5. {¬r(x)} 3,4
6. {q(x)} 2,5

So I am in 5th step and I can't proceed further. is there any way that I can say c and x and equal and prove the given formula is unsatisfiable? I am confused. Can someone clear my doubt?

Answer 1

Yes, that's exactly what you need to do: you 'unify' $q(x)$ and $\neg q(c)$ by substituting $c$ for $x$, and thus you get the empty clause.

You can do this because any variables that end up in the clauses come from universals, and so you can fill in any term for those variables you want, as long as you use that substitution systematically. That is you can 'unify' $q(x)$ and $\neg q(c)$, and also $q(x)$ and $\neg q(y)$, but not $f(x,x)$ and $f(a,b)$.

This process is called unification and is an important part of Resolution ... I am surprised you didn't run into that yet.