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

標(biāo)準(zhǔn)式的化簡(jiǎn)步驟
　　如果一個(gè)合適公式的所有量詞均非否定的出現(xiàn)在公式的前部，而且所有的量詞的
　　約束范圍均是整個(gè)公式，則稱這樣的合適公式為前束范式。任何一個(gè)合適公式，
　　都可以等價(jià)地轉(zhuǎn)化為一個(gè)前束范式。消去前束范式中所有的存在量詞后得到的
　　合適公式，稱為S范式，這一過(guò)程稱作skolem化。S范式與它的原式不一定等價(jià)，
　　但在不可滿足性方面，二者是等價(jià)的。也就是說(shuō)，如果原式是不可滿足的，
　　則其對(duì)應(yīng)的S范式也一定是不可滿足的。反之亦成立。

（1）消蘊(yùn)涵符

（2）移動(dòng)否定符
如果公式中的否定符"～"不只是作用于原子公式，則要利用摩根定律對(duì)公式進(jìn)行變換，
使得否定符只作用于原子公式。

如果否定作用于量詞的話，可以用量詞轉(zhuǎn)換律將量詞提到否定的作用域之外。

（3）變量換名

（4）量詞左移
將所有的量詞移到公式的左邊，但不改變?cè)瓉?lái)各量詞的排列順序。
這也是為什么在第三步要進(jìn)行變量改名的原因，否則就不能進(jìn)行這種移動(dòng)。

（5）消去存在量詞（skolem化）
按照這樣的原則將公式中的存在量詞消去：設(shè)E是前束范式中的一個(gè)存在量詞，
如果在它的前面沒(méi)有出現(xiàn)全稱量詞，則所約束的變量x，全部用一個(gè)新的常量
（未在公式中出現(xiàn)過(guò)）代替；如果E前面有全稱量詞，則所約束的變量x，
全部用一個(gè)新的（未在公式出現(xiàn)過(guò)的）函數(shù)（稱為skolem函數(shù)）代替，該函數(shù)的
變量是哪些在前面的全稱量詞所約束的變量。然后將存在量詞E消去。

（6）化為合取范式
利用結(jié)合律、分配律等，可以把S范式的母式轉(zhuǎn)化為合取范式。
A(x)∨(B(x)∧C(x)) ≡ (A(x)∨B(x))∧(A(x)∨C(x))

（7）隱去全稱量詞
經(jīng)過(guò)前6步變換以后，所有的變量都是受全稱量詞約束，所以可以將全稱量詞隱去，
默認(rèn)所有的變量是受全稱量詞約束的。

（8）表示為子句集
在隱去全稱量詞以后，用"，"號(hào)代替公式中的"∧"，并用"{"和"}"括起來(lái)，就得到了
原合適公式的子句集。

（9）變量換名
對(duì)子句集中的變量再次進(jìn)行換名替換，使得不同的子句中的變量使用不同的名字。
最簡(jiǎn)單的方法是采用加下標(biāo)的方法。注意：在有些書(shū)中并不要求對(duì)子句集中的變量
進(jìn)行換名替換，如果是這樣的話，你必須很清楚，不同子句中的變量，即便是同名的，
也可以代表不同的變量。在后邊將要介紹的歸結(jié)法中，你會(huì)發(fā)現(xiàn)，如果不進(jìn)行換名，
很容易出現(xiàn)錯(cuò)誤。因此建議大家對(duì)變量進(jìn)行換名。由于每一個(gè)子句都對(duì)應(yīng)一個(gè)不同的
合取元，變量都由全稱量詞量化，因而實(shí)質(zhì)上兩個(gè)子句的變量之間不存在任何關(guān)系，
這里的變量換名不影響公式的真值。

---------------------------------------------------
Skolem化并不影響原合適公式的永假特性
---------------------------------------------------