3
$\begingroup$

I know I am making a mistake somewhere but consider the following truth table:

p0   p1   p2  | ------------------- 0    0    0   | 1   0    0    1   | 0   0    1    0   | 0   0    1    1   | 1   1    0    0   | 1   1    0    1   | 1   1    1    0   | 1   1    1    1   | 1 

This coresponds to the boolean formula in DNF:

p0 v (~p1 ^ ~p2) v (p1 ^ p2) 

or in CNF:

(p0 v ~p1 v p2) ^ (p0 v p1 v ~p2) 

Using the last two clauses and applying the resolution inference rule on p1:

(p0 v ~p1 v p2) ^ (p0 v p1 v ~p2) |- (p0 v p2 v ~p2) = (p0 v T) = p0 

So from the two clauses I can infer p0. This does not seem right since p0 does not always have to be true according to the truth table.

1 Answers 1

6

Your mistake is that $(p_0 \vee T) = T$ and not $p_0$ as you wrote.

In fact it is provable from the empty set that $(p_0 \vee p_2\vee\neg p_2)$.

  • 0
    You are right. What a newbie mistake. My head was spinning for the last hour :)2011-03-07