In the case where the algorithm is terminated with the answer yes, that is the case where

I cannot add more clauses to my CNF by resolution.

In the case where we can no longer add new resolvents

and also where phi does not contain the empty clause at the moment, the algorithm says yes.

We have to show that this means that phi is achievable.

We do this by induction over the number of propositional atoms in phi.

The induction beginning is trivial.

There are only two CNFs in the number writing method that I can even form without atoms.

I have excluded one of them, namely the one that contains the empty clause.

The only thing that remains is the CNF that does not contain the empty clause.

The induction step remains, which is one from less than n to n.

We take one atom that is present in phi, eliminate it and we have fewer atoms.

We can apply the induction conditions in this way.

We have defined the following two CNFs.

This is something that we call phi-attached A, which consists of a clause CNPhi,

from which I remove the negation of A.

If I accept A, I can no longer add anything to the completion of the clause.

I only keep clauses that do not contain A.

We take the negation of phi, which is C without A, where A is not a C and C is from phi.

These are the two clauses that can be applied to the induction conditions.

The reason is that they contain one atom less than the other.

The induction conditions are an implication.

To have something of this, I have to show that one of the two has fulfilled the assumption.

Let's start with the simple one.

It is not necessarily the case that the empty clause is not in both.

I think that phi is simply this.

Let's see what happens with phi-attached A.

I keep the one clause that is in the clause CNPhi, because it does not contain A.

I remove A from this clause and the empty clause remains.

I can not rely on the fact that both do not contain the empty clause.

But I think that at least one of the two will not contain the empty clause.

Let's assume that both cases contain the empty clause.

Let's start with A.

The empty clause is created. Phi does not contain the empty clause.

The empty clause must contain phi.

Now, because phi is closed, we can solve these two clauses.

What remains is the empty clause.

Both cases are symmetrical.

Let's say that phi-attached A is closed.

I take two clauses in phi-attached A that I can solve.

I take two clauses in phi-attached A that I can solve.

One clause contains a positive and one clause contains a negative.

A moment of reflection reveals that this literal is not this A.

We have C1 combined with a quantity B.

So it must be in phi and A must not contain it.

C2 is not combined with B.

This is our general situation where we can solve two clauses in phi-attached A.

What is the result of the solution?

The B's are eliminated.

The C's remain.