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