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?


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.