对任一合式公式可通过以下各步化成前束范式：
（1）消去多余的前束（量词）。这在化简过程都要随时注意到，因为可能出现母式中没有其前束中相对应的约束变元，因而这个前束是多余的，应及时消去。
（2）消去蕴涵符号（"→"联结词）。反复使用具有"→"联结词的等值公式，把公式中所有的"→"都消去。
（3）内移否定词~的辖域范围。反复使用摩根定律和量词互换式，把否定词标到只作用于原子公式为止。
（4）变量标准化。对变量作必要的换名，使每一量词只约束一个唯一的变量名。由于变量名可任意设定，因而该过程不影响合式公式的真值。
（5）把所有量词都集中到公式左面，移动时不要改变其相对顺序。
（6）消去存在量词。对于待消去的存在量词，若不在任何全称量词辖域之内（即它的左边没有全称量词），则用Skolem常量替代公式中存在量词约束的变量，若受全称量词约束（即左边有全称量词），则要用Skolem函数（即与全称量词约束变量有关的函数）替代存在量词约束的变量，然后就可消去存在量词。例如公式
F＝（x）（y）（z）（u）（v）（w）（P（x，y，z，u，v，w）
∧（Q（x，y，z，u，v，w）∨~R（x，z，w）））
其中母式各变量中，四个存在量词所约束的变量应分别用如下所示的Skolem函数和常量替代：
x＝a，y＝b，u＝f（z），w＝g（z，v）
消去存在量词后得
F1＝（z）（v）（P（a，b，z，f（z），v，g（z，v））
∧（Q（a，b，z，f（z），v，g（z，v））∨~R（a，z，g（z，v）））
（7）把母式化成合取范式。反复使用结合律和分配律，将母式表达成合取范式的标准型，最后得到一个Skolem化的前束范式Fs。
（8）隐略去前束式。由于母式的变量均受量词的约束，可省略掉全称量词，但剩下的母式仍假设其变量受全称量词量化。
（9）把母式用子句集表示。把母式中每一个合取元称为一个子句，省去合取联结词，这样就可把母式写成集合的形式表示，每一个元素就是一个子句。如上例的子句集是
S＝{P（a，b，z，f（z），v，g（z，v）），
Q（a，b，z，f（z），v，g（z，v））∨~R（a，z，g（z，v））}
（10）子句变量标准化。将子句集中的变量作分离标准化，即对某些变量重新命名，使任意两个子句不会有相同的变量出现。由于每一个子句都对应一个不同的合取元，变量都由全称量词量化，因而实质上两个子句的变量之间不存在任何关系，变量标准化不影响公式的真值。变量标准化这个步骤很重要，这是因为在使用子句集进行证明推理过程，有时要例化某一个全称量词量化的变量（即用某一特定值替代变量），这时就可能使公式尽量保持其一般化形式，增加了应用过程的灵活性。

　　3．标准式的应用问题
　　经上述步骤化简得到的标准式是经过Skolem化的前束范式，通常也称为S-标准形。要注意S-标准形不是唯一的，若把它记为Fs，则Fs仅仅是F（未Skolem化的前束式）的一个特例，取用不同的Skolem函数会得到不同的结果。当F为非永假公式时，Fs与F并不等价，但当F为永假时，Fs也一定是永假的，即Skolem化并不影响F的永假特性。这个结论很重要，可用定理形式描述如下，它是下面将要讨论的归结原理的主要依据。
　　定理：若S是合式公式F的S-标准形之子句集，则F为永假的充要条件是S为不可满足的。
　　上面已经提到过子句的概念，它是S-标准形母式中的合取元，因而每一个子句是若干文字（或基本式，即原子公式和原子公式否定式组成集合中的任一元素）的析取式。不含有文字的子句称为空子句，显然空子句是一种没有任何能满足某种解释的子句，即空子句的取值总为假，一般简记为□或NIL。一个子句的文字中，其变量被常量替代，就得到一个文字的基例，由基文字组成的子句称基子句。
　　子句集中所有元素（即子句）的合取式不为真，则称该子句集为不可满足的。
　　最后还应指出谓词演算体系中还有一些很重要的概念，如谓词演算的可判定性问题、逻辑推论、推理规则的有效性、推理规则系统的完备性等等，对人工智能推理机制的研究都很有用。本章只从产生式的角度来讨论谓词演算的应用问题，至于涉及更深入的基本理论可参阅数理论逻辑的有关著述。