参考自http://www.ycrc.com.cn/qinghua/18/text/chapter4/section1/1.htm

标准式的化简步骤
　　如果一个合适公式的所有量词均非否定的出现在公式的前部，而且所有的量词的
　　约束范围均是整个公式，则称这样的合适公式为前束范式。任何一个合适公式，
　　都可以等价地转化为一个前束范式。消去前束范式中所有的存在量词后得到的
　　合适公式，称为S范式，这一过程称作skolem化。S范式与它的原式不一定等价，
　　但在不可满足性方面，二者是等价的。也就是说，如果原式是不可满足的，
　　则其对应的S范式也一定是不可满足的。反之亦成立。

（1）消蕴涵符

（2）移动否定符
如果公式中的否定符"～"不只是作用于原子公式，则要利用摩根定律对公式进行变换，
使得否定符只作用于原子公式。

如果否定作用于量词的话，可以用量词转换律将量词提到否定的作用域之外。

（3）变量换名

（4）量词左移
将所有的量词移到公式的左边，但不改变原来各量词的排列顺序。
这也是为什么在第三步要进行变量改名的原因，否则就不能进行这种移动。

（5）消去存在量词（skolem化）
按照这样的原则将公式中的存在量词消去：设E是前束范式中的一个存在量词，
如果在它的前面没有出现全称量词，则所约束的变量x，全部用一个新的常量
（未在公式中出现过）代替；如果E前面有全称量词，则所约束的变量x，
全部用一个新的（未在公式出现过的）函数（称为skolem函数）代替，该函数的
变量是哪些在前面的全称量词所约束的变量。然后将存在量词E消去。

（6）化为合取范式
利用结合律、分配律等，可以把S范式的母式转化为合取范式。
A(x)∨(B(x)∧C(x)) ≡ (A(x)∨B(x))∧(A(x)∨C(x))

（7）隐去全称量词
经过前6步变换以后，所有的变量都是受全称量词约束，所以可以将全称量词隐去，
默认所有的变量是受全称量词约束的。

（8）表示为子句集
在隐去全称量词以后，用"，"号代替公式中的"∧"，并用"{"和"}"括起来，就得到了
原合适公式的子句集。

（9）变量换名
对子句集中的变量再次进行换名替换，使得不同的子句中的变量使用不同的名字。
最简单的方法是采用加下标的方法。注意：在有些书中并不要求对子句集中的变量
进行换名替换，如果是这样的话，你必须很清楚，不同子句中的变量，即便是同名的，
也可以代表不同的变量。在后边将要介绍的归结法中，你会发现，如果不进行换名，
很容易出现错误。因此建议大家对变量进行换名。由于每一个子句都对应一个不同的
合取元，变量都由全称量词量化，因而实质上两个子句的变量之间不存在任何关系，
这里的变量换名不影响公式的真值。

---------------------------------------------------
Skolem化并不影响原合适公式的永假特性
---------------------------------------------------