# A case of theorem proving through resolution

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.

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