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

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. — Shailesh, Feb 11 '16 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. — Mauro ALLEGRANZA, Feb 11 '16 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)$ — Graham Kemp, Feb 12 '16 at 2:12
@GrahamKemp ok i see that I interpretated the distrubution law wrong, thanks — coders, Feb 12 '16 at 16:02

Mauro ALLEGRANZA · Accepted Answer · 2016-02-12 19:00:23Z

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

1 Answer 1