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, 2016 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$ Feb 11, 2016 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$ Feb 12, 2016 at 2:12
  • $\begingroup$ @GrahamKemp ok i see that I interpretated the distrubution law wrong, thanks $\endgroup$ Feb 12, 2016 at 16:02

1 Answer 1


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.