Prove that a sentence is a tautology using resolution

Question

I have the following sentence.

$(A ∨ (B ∧ C) ∨ (¬A ∧ ¬B) ∨ (¬A ∧ B ∧ ¬C))$

I am having difficulty understanding how to apply the resolution method.

---

What (I think) I know so far:

In terms of resolution as it applies to my problem, it seems I am considering the resolution technique (of propositional logic).

Given the resolution technique in the following form:

$$\underline{\{Q ∧ O\} \ \{¬O\}}$$ $$Q$$

To put it in my own words, the resolution technique reduces a sentence to a set of clauses of literals and considers which what the value of each literal would have to be such that the conjunction of each clause would be true. So in my cause I need to:

1. Rearrange my sentence to a set of clauses.
2. Determine the value for each literal, using the technique above.
3. Use the information from step 2 to determine weather the sentence is a tautology (I don't know how to do this).

Am I on the right track? Any tips?

Answer 1

See Resolution (logic) :

the resolution technique uses proof by contradiction and is based on the fact that any sentence in propositional logic can be transformed into an equivalent sentence in Conjunctive Normal Form.

1st step :

the negation of the sentence to be proved (the conjecture) is to be considered.

In your case, we have :

$$\lnot [A ∨ (B∧C) ∨ (¬A∧¬B) ∨ (¬A∧B∧¬C)] \equiv [¬A ∧ (¬B ∨ ¬C) ∧ (A ∨ B) ∧ (A ∨ ¬B ∨ C)].$$

As said above, the proof procedure works by contradicition : assume the formula $\lnot \varphi$ (where $\varphi$ is the conjecture) and apply iteratively the rule.

If the procedure gives us as result that the formula $\lnot \varphi$ is unsatisfiable, we can conclude that the original conjecture ($\varphi$) is a tautology.

2nd step :

the sentence is transformed into a Conjunctive Normal Form with the conjuncts viewed as elements in a set, $S$, of clauses, where a clause is a disjunction of literals.

Thus, the formula above will correspond to the set of clauses :

$S = \{ ¬A, (¬B ∨ ¬C), (A ∨ B), (A ∨ ¬B ∨ C) \}$.

3rd step :

The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set $S$, it is added to $S$, and is considered for further resolution inferences.

If after applying a resolution rule the empty clause, $\square$ (or : $\bot$), is derived, the original formula is unsatisfiable (or contradictory), and hence it can be concluded that the initial conjecture is a tautology.

We have to apply the rule to the set $S$ above :

1) $¬A$

2) $¬B ∨ ¬C$

3) $A ∨ B$

4) $A ∨ ¬B ∨ C$

5) $B$ --- from 1) and 3)

6) $¬B ∨ C$ --- from 1) and 4)

7) $¬C$ --- from 5) and 2)

8) $C$ --- from 5) and 6)

$\square$ --- the empty clause : from 7) and 8).

The rule has the property that preserves satisfiability, i.e. the new set of clauses is satisfiable iff the original one is.

Thus, if after iterated applications of the rule the empty clause is produced, being it unsatisfiable (the empty clause in another way of representing a contradiction) this is enough to conclude that also the original set of clauses is unsatisfiable.