Resolution Refutations
Now let us resolve the following clause
{(ᆨA, B), (ᆨA, ᆨB, C), A, ᆨC)
We begin by resolving the first clause with the second Clause, thus eliminating B and ᆨB
{(ᆨA, C), A, ᆨC}
{C, ᆨAC}
⊥
The fact that this resolution has resulted in falsum. means that the original clauses were inconsistent. We have refutated the, original, clauses, using resolution refutation. We can write,
{(ᆨA, B), (ᆨA, ᆨB, ᆨC), A, ᆨC) ⊨ ⊥
Proof by Refutation: Proof by refutation (also known as proof by contradiction) as used in resolution refutation, is a powerful method; for solving problems. For example, Let us imagine that we want to determine whether the following logical argument is valid or not.
If it rains and I don't have an umbrella, then I will get wet,
It is raining and I don't have an umbrella,
Therefore, I will get wet.
We can rewrite this in propositional calculus as follows,
(A Λ ᆨB) ⟶ C
A Λ ᆨB
∴ C
To prove this by refutation, we first negate the conclusion and convert the expressions into clause form. The first expression is the only one that is not already in CNF, so first we convert this to CNF as follows,
(A â´· ᆨB) ⟶ C
= ᆨ(A â´· ᆨB) ⋁ C
= ᆨA ⋁ B ⋁ C
Now, to prove that our conclusion is valid, we need to show that,
{(ᆨA, B, C), A, ᆨB, ᆨC} ⊨ ⊥
We resolve these clauses as follows,
{(B, C), ᆨB, {C, ᆨC}
⊥
Hence, in showing that by negating our conclusion, we lead to a contradiction, we have shown that our original conclusion must have been true.
If this process leads to a situation where some clauses are unresolved, and falsum cannot be reached, we have shown that the clauses with the negated conclusion are not contradictory and therefore the original conclusion was not valid.
Because following resolution explanations in this way can be confusing it is often preferable to present a resolution proof in the form of a tree, where, pairs of resolved clauses are connected together, as shown in the following proof.
A ⟶ B
B⟶ C
C ⟶ D
D⟶ E ∨ F
A ⟶ F
First, we negate the conclusion, to give ᆨ(A ⟶ F) Next we convert to clause form,
D⟶ E ∨ F
≡ ᆨD ∨ (E ∨ F)
and ᆨA ⟶ F
≡ ᆨ(ᆨA ∨ F)
≡ A ∧ F
So our clauses are,
{(ᆨA, B), (ᆨB, C), (ᆨC, כ), (ᆨD, E, F), A, ᆨF}
Our proof in tree form is as follows,
Fig: A Resolution Refutation Tree
We have not been able to reach falsum because we are left with a single clause {E}, which cannot be resolved with any thing. Hence, we can conclude that our original conclusion was not valid. You can prove this for yourself using a truth table.
