【摘要】：为了总结我们关于归结的讨论，现在我们将说明为什么PL-RESOLUTION是完备的。PL-RESOLUTION所演算并作为变量clauses终值的就是归结闭包。容易看出，RC一定是有限的，因为，用S中出现的符号P1，…（注意，如果没有将重复的文字剔除的归并步骤，这可能不成立。）因此，PL-RESOLUTION总是可终止的。, Pk的适当真值构造S的一个模型。构造过程如下：— 如果 RC中有一个包含文字Pi的子句，该子句所有的其它文字在 P1，…还需要证明对P1，…证明过程留作一道习题。
为了总结我们关于归结的讨论，现在我们将说明为什么PL-RESOLUTION是完备的。为了做到这一点，我们需要介绍子句集S的归结闭包RC(S)，它是通过对S中的子句或其派生子句反复应用归结规则而生成的所有子句的集合。PL-RESOLUTION所演算并作为变量clauses终值的就是归结闭包。容易看出，RC(S)一定是有限的，因为，用S中出现的符号P1，…，Pk只能构成有限多个不同的子句。（注意，如果没有将重复的文字剔除的归并步骤，这可能不成立。）因此，PL-RESOLUTION总是可终止的。
命题逻辑中归结的完备性定理被称为基本归结定理：
如果子句集是不可满足的，那么这些子句的归结闭包包含空子句。
我们通过证明这个定理的逆否命题：如果闭包 RC(S)不包含空子句，那么 S 是可满足的，来证明这个定理。实际上，我们可以用P1, … , Pk的适当真值构造S的一个模型。构造过程如下：
i从1到k，
— 如果 RC(S)中有一个包含文字¬Pi的子句，该子句所有的其它文字在 P1，…，Pi−1的赋值下都为假，那么对Pi赋值false。
— 否则，对Pi赋值true。
还需要证明对P1，…，Pk的赋值是S的一个模型，倘若RC(S)在归结下是封闭的而且不包含空子句的话。证明过程留作一道习题。
免责声明：以上内容源自网络，版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。
