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.



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


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$.


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.