Resolution calculus converting into set of clauses

Question

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

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$.