Here is $T$:

  • $a \lor \neg b$
  • $\neg a \lor (c \land d)$
  • $b$

I am suppose to use resolution calculus to prove that $T \models d \land b$ holds.

As in the first step, we translate $T$ into a set of clauses, all clauses being in CNF.

My lecturer converts $T$ into the following clauses:

Clause 1: $\neg a \lor \neg b$

Clause 2: $a \lor c$

Clause 3: $a \lor d$

Clause 4: $b$

Clause 1 and clause 4 seem correct to me (in CNF).

But howcome $\neg a \lor (c \land d)$ in $T$ becomes into Clause 2 & 3 ($a \lor c$, $a \lor d$)?

Shouldn't it be $(a \land c) \lor (a \land d)$ (distribution law)?

  • $\begingroup$ Your professor is correct in applying the distributive law. Secondly there is an error in Clause 1 and what you have written earlier (the 'not' sign before $a$ is missing. $\endgroup$ – Shailesh Feb 11 '16 at 16:47
  • $\begingroup$ @Shailesh - wy do you think that $¬a \lor (c \land d)$ is equivalent to $(a \lor c) \land (a \lor d)$ ? see Distributive property. $\endgroup$ – Mauro ALLEGRANZA Feb 11 '16 at 17:51
  • $\begingroup$ The distribution is: $\quad\large\color{red}{\neg a~\vee~}(c\color{blue}{~\wedge~}d) \;\dashv\vdash\; (\color{red}{\neg a~\vee~}c)\color{blue}{~\wedge~} (\color{red}{\neg a~\vee~}d)$ $\endgroup$ – Graham Kemp Feb 12 '16 at 2:12
  • $\begingroup$ @GrahamKemp ok i see that I interpretated the distrubution law wrong, thanks $\endgroup$ – coders Feb 12 '16 at 16:02

After having corrected the wrong application of the distribution law, we have the following clauses:

Clause 1: $a ∨ ¬b$

Clause 2: $\lnot a ∨ c$

Clause 3: $\lnot a ∨ d$

Clause 4: $b$

and the negation of the formula to be proved:

5) $\lnot d \lor \lnot b$.

Now we have to apply resolution, starting with 4)-1) and 4)-5) deriving:

6) $a$

7) $\lnot d$.

Then we have to use 7)-3) to derive:

8) $\lnot a$.

Finally, using 6) and 8) we conclude with the empty clause: $\bot$.


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.