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