Completeness resolution

To complete the discussion of the resolution rule in this section, let us show why the PL-Resolution algorithm is complete. To do this, it is advisable to introduce the concept of the resolution closure RC (S) of the set of expressions, which is the set of all expressions that can be obtained by reapplying the resolution rule to expressions from the set S or to their derivatives.

The resolution closure is a set of expressions, which is computed by the PL-Resolution algorithm as the final value of the clauses variable. It can easily be shown that the set RC (S) must be finite, since the number of different expressions that can be formed from the symbols P ₁ , ... P _k present in S is finite. (It should be noted that this statement would not be true if the factorization stage were not used, in which additional copies of literals are destroyed.) Therefore, the PL-Resolution algorithm always finishes its work.

Part of a flowchart showing the process of applying the PL-Resolution function to form a simple inference in the vampus world . Here it is shown that from the first four expressions given in the top row, follows the expression ¬P1,2

The completeness theorem for the rule of resolution in propositional logic is called the main theorem of the resolution . If the set of expressions is impracticable, then the resolution closure of these expressions contains an empty expression. We prove this theorem by showing that the opposite statement is true: if the closure RC (S) does not contain an empty expression, then the set S is satisfiable. In fact, for a set of S, you can create a model with suitable truth values ​​for P ₁ , ..., P _k . The procedure for creating such a model is described below. For i from 1 to k:

• if the set RC (S) contains an expression containing the literal ¬P _i , such that all its other literals are false with the given assignment chosen for P ₁ , ... P _{i -1} , then set the literal P _i to false; otherwise, set the literal P _i to true.
• It remains to show that this is the assignment of values ​​to literals Pr, ..., Pk