參考自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化并不影響原合適公式的永假特性
---------------------------------------------------