1
$\begingroup$

we have to clauses: $$\{\neg A(y_1, z_1), A(x_1, z_1) \} \\ \{\neg A(x_2, z_2), A(y_2, z_2)\}$$

  1. can I resolve it to an empty clause? Exactly, I would like to know whether I can make a resolvent removing two negated literals from every set.

  2. Is set of clauses $\{A(z_1, z_2), A(z_3, z_4)\}$ equivalent to $\{A(z_1, z_2)\}$ in the sense of resolution proof?

$\endgroup$

Your Answer

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

Browse other questions tagged or ask your own question.