1.消去蕴含等价

2.将否定符号移动到紧靠谓词的位置上

3.变量标准化

即，不同含义的变量用不同字母。

4.消去存在量词

分两种情况：存在量词出现在一个或者多个全称量词辖域内；存在量词不出现在全称量词辖域内。

5.化为前束式

{全称量词串}（不含全称量词的式子）

6.化为skolem标准型

7.略去全称量词

即，全称量词串直接省略不写。

8.消去合取连接词

9.字句变量标准化

即，不同的字句用不同的变元。

（只做1-5化为前束形）