说明 　　(1) S并不是A的母式的特例集合，而是A的无前束范式A'的母式的特例集合。 　　(2) S不含任何量词，变元。令B(t1,t2,…, tm)∈S ,B(t1,t2,…, tm) 可以写成CNF, 其中的每一文字是L中的原子公式或原子公式的否定。所谓L的原子公式是P(t1,t2,…, tk) 或者F(t1,t2,…, tk) = tk+1 。 　　(3) H 可以归纳地定义为 　　H0= {t'│t是在A'中出现的常项符号及自由变元符号，如果二者都不在A'中出现，引入一个新的常项符号c ,H0由c组成 } 　　Hn+1 =Hn∪{ F(t1,t2,…, tm)│ t1,t2,…, tm∈Hn ，F在A'中出现。} 　　H=∪Hn , n 遍历所有的整数。 　　注意到A'是 L 的一个给定的公式，它的符号集合是有穷的，因而 H0是有穷的。同时，在A'中也只出现有穷个函词符号，因而每一个 Hn 都是有穷的。按H的这个分层，可以在一个有效的可数过程中逐个检查 S 的每一个有穷子集合 S' 。由 (2) 及关于命题演算公式的归结方法，对每一 S' 的归结，不管 S'是否可满足，一定终止，然后对下一个 S 的有穷子集合进行命题演算的归结过程。由 Herbrand 定理，如果A是不可满足的，则在有穷步内，一定能找到一个不可满足的有穷子集合，从而过程终止。但如果A是可满足的，则过程永远不停止，就永远不能肯定A是否可满足。所以这个判定方法是"半可判定"算法，也叫做"非确定性算法"。 　　相当一部分的国内外计算机科学和人工智能专家都认为，在大部分的计算复杂性很高的计算问题中，非确定性的算法往往比确定性算法有效得多、实用得多。应该指出，非确定性算法的研究，仍然有待进一步的、深入的研究。 　　由于M│ =A , 按照 Lowenheim-Skolem 定理证明中构造理M的初等子模型的方法，将N扩充为M的子模型，该子模型满足A。注意按 7.4.2的说明，该构造过程，对A的每一个量词，都可以顺势定义N上的一个函数f , 它的变元是所有该符号左边出现的被"形的量词约束的变元。同样，令第一次扩充的结果是N* ,N0=N ,Nk+1=Nk* ,H=∪Nk , k遍历所有的整数。可以验证，A的无前束范式A'的母式B(x1,x2,…, F1, xk+1,…,F2, …,xm) 的任一特例在 H 中都是成立的。因此H│= S 。 S 是可满足的，由紧致性定理，S 的每一个有穷子集合都是可满足的。 　　同样用反证法。假定S的任一有穷子集合 S'都是协调的，则 S 是协调的。根据定理 7.3.2 的证明中的引理 2 及其证明方法，同样可以建立 S 的一个形式模型M, 它的论域是A'的 Herbrand 域的一个子集合，而且每一个引入的新的函词符号F都在M上有解释。用简单的归纳法，施归纳于A的前束式的复杂性，可以验证，M同样是A的一个模型。所以A是可满足的。