Show by Resolution that a set of clauses is unsatisfiable

Question

Im trying to show by resolution that the following set of clauses is unsatisfiable:

$\{ p(x,f(y)) \lor p(c,z), ¬p(y,f(f(y))) \lor ¬p(c,x) \}$.

Now, I know that to show the unsatisfiability I need to derive an empty clause from the original clause set. So far Ive only done exercises with at least one clause having just one literal. This time I dont understand how I can end up with empty clause when theres always two literals.

Answer 1

Hint

In order to apply Resolution to predicate logic, you have to use Unification.

Step 1) : use the substitution $z \leftarrow x$ with $¬p(c,x)$ to get $¬p(c,z)$ and resolve with: $p(x,f(y)) \lor p(c,z)$ to get

$p(x,f(y))$.

Now you have to clauses : $p(x,f(y))$ and $¬p(y,f(f(y)))$.

Find a suitable substitution to unify them and you wll get the empty clause : $\square$.