# Resolution calculus converting into set of clauses

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)?

• 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. Feb 11, 2016 at 16:47
• @Shailesh - wy do you think that $¬a \lor (c \land d)$ is equivalent to $(a \lor c) \land (a \lor d)$ ? see Distributive property. Feb 11, 2016 at 17:51
• 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)$ Feb 12, 2016 at 2:12
• @GrahamKemp ok i see that I interpretated the distrubution law wrong, thanks Feb 12, 2016 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$.