Logic proof: Prove The Completeness of the Resolution Process

Question

In our Logic course in computer science, our professor showed a proof to the "completeness of the resolution process" for propositional logic and I could not understand it well. Because the language used is Hebrew I cannot copy paste into here, but in general what was written in that proof was that if the empty clause is not a part of some formula $A$ then $A$ is satisfiable.

When the clause is of the form: $\{ \{p\}, \{ \neg p\} \}$, we call it the "$\text {empty clause}$".

The proof the professor used was in "induction on the number of atoms in $A$" showing that for the basic step of the induction, the theorem is correct because for $A$ with only one atom, only $\{ \{p\}, \{\neg p\} \}$ isn't satisfiable and therefore the theorem holds.

The inductions premise was that for any formula $A$ with less than $N$ atoms, if the empty clause is not a part of $A$ then $A$ is satisfiable, and the step was: to prove it holds for the case of $A$ with $N$ atoms.

Answer 1

Prliminaries

Resolution is a proof procedure.

Completeness - for the propositional case - means that :

If the formula $X$ is a tautology, $X$ has a resolution proof.

A resolution proof of $X$ starts from $\lnot X$ and try to derive the empty clause : $\bot$ or $\square$.

The proof relies on the fact that a formula $X$ is a tautology iff $\lnot X$ is unsatisfiable and on the soundness of the Resolution rule :

a rule is sound when the conclusion of the rule is a logical consequence of the premises;

that implies that if the premises are satisfiable also the conlusion is.

Applied to resolution, we have that the empty cluase : $\bot$ is unsatisfiable; thus, a proof ending with $\bot$ proves that the starting formula $\lnot X$ is also unsatisfiable, which amounts to proving that $X$ is a tautology.

---

Proof sketch

The "completeness problem" is:

Is every tautology provable by the resolution method?

Stated otherwise, if $X$ is a tautology, can we be sure that after a finite number of application of the resolution rule starting with $\lnot X$ we will reach the empty clause: $\bot$ ?

To prove it, we need a basic lemma :

a set of clauses that does not include $\bot$ (i.e. an inconsistent pair : $p, \lnot p$) is satisfiable.

This - I think - is what your teacher showed during the course.

The "finitiness" requirement is ensured by the fact that every application of the rule reduces the number of literals in the clauses.

Having proved the above result, completeness follows:

suppose that we have completed the resolution procedure (i.e. no more applications of the rule are possible) for the formula $\lnot X$. If the final clause does not include $\bot$, then $\lnot X$ is satisfiable, by the above lemma. Hence $X$ cannot be a tautology.

Thus, if $X$ is a tautology, the resolution procedure must terminate with $\bot$.