Skolem標(biāo)準(zhǔn)型是Skolem于1920年提出的一個(gè)使一階公式標(biāo)準(zhǔn)化的方法，其定義如下：Skolem標(biāo)準(zhǔn)型是如下任意一種形式的一階命題：(1)?x1?x2...?xm?y1?y2...?ynUx1x2...xmy1y2...yn(∏Σ型 )；(2)?x1?x2...?xmUx1x2...xm(∏型)；(3)?x1?x2...?xmUx1x2...xm(Σ型)。其中，U是不包含量詞且連接符僅僅為∧，∨，→的公式。

外文名

Skolemstandardmodel

所屬學(xué)科

數(shù)學(xué)

基本介紹

定義1

Skolem標(biāo)準(zhǔn)型是如下任意一種形式的一階命題：

(∏∑型)

（1）

(∏或∑型 )

(2)

(∏型)

(3)

(∑型)

其中，U是不包含量詞且連接符僅僅為

的公式。

第(1)種標(biāo)準(zhǔn)型顯然借鑒了亞里士多德三段論的直言命題的形式。第(1)、(3) 種標(biāo)準(zhǔn)型中的

是可以消除的。消除的方法有三種。第一種是將公式中的

換為

，然后對于原來

的約束項(xiàng)變?yōu)樗懊娴淖兞看_定的新的變量，這樣原來的公式成為僅由全稱量詞約束的公式，原來的存在量詞約束的項(xiàng)的解釋縮小為由它前面的項(xiàng)所確定的量

。如

轉(zhuǎn)換為

，也可寫成

。如果有明確的y的解釋域，這種轉(zhuǎn)換后新的公式?jīng)]有改變與原有公式的真假值的等價(jià)性；否則真假值的等價(jià)性可能有變。第二種是將(1)公式中的

換為

，然后對于對U增加解釋性的關(guān)系，使得公式對于原來公式的域中不能滿足的

的項(xiàng)增補(bǔ)一個(gè)非關(guān)系，進(jìn)而擴(kuò)大了y 的解釋域。第三種是將公式中的

去掉，然后對于原來的約束項(xiàng)變?yōu)橐粋€(gè)確定的解釋域中的項(xiàng)a，原有公式的真假值的等價(jià)性遭到破壞，但是在確定公式的無效性(永假) 時(shí)，改變后的公式與原公式具有同等意義。無論哪種方法都可以消除存在量詞

。用上述同樣的方法，顯然，也可以將一階公式轉(zhuǎn)換為標(biāo)準(zhǔn)型(注意轉(zhuǎn)變后其有效性可能與原公式并不完全等價(jià))。

總之，對于一階命題(公式)的Skolem 標(biāo)準(zhǔn)化，是基于

Skolem 標(biāo)準(zhǔn)化的定理

：對于任何一階命題A，都存在一個(gè)標(biāo)準(zhǔn)型命題

，使得當(dāng)

是可滿足的，A在其解釋域是可滿足的。

定理1

一階公式G 與G的子句集S并不相等，但是它們具有相同的不可滿足性。

證明:

如果公式G 是∏型，解釋G 的域

，這與子句集解釋S的域完全重合。同時(shí)，G 不能滿足，也就意味著

中至少有一個(gè)子句不能滿足，此時(shí)

為0；由于

，此時(shí)S也為0，即Ⅱ型的不可滿足性與子句集S的不可滿足性完全相同。

如果公式G 是∏∑型或∑型，此時(shí)G將有

約束的項(xiàng)

，如果子句集中對于

的解釋域設(shè)置為

將與

的解釋域可能不一致。但是，對于不可滿足性而言，“沒有任何一個(gè)解釋滿足G 中

構(gòu)成的公式”和“

均不可滿足S中

構(gòu)成的公式”在邏輯上是一致的?？蓞⒄罩毖悦}量詞的否定運(yùn)算規(guī)則，即

，它是說，“不存在”(即的不可滿足性) 意味著“

”所描述的(與

約束的項(xiàng)的)域“全都不”滿足。“

”是表述在G中：而“

”表述在子句集中——因?yàn)樽泳洳辉俦硎玖吭~約束意味著以項(xiàng)的全稱為解釋域，

恰好表達(dá)了所有解釋的不滿足性。

定理1的啟示在于，對于∏∑型或∑型的一階公式，如果證明其不可滿足性，可以證明其替換

之后形成的Ⅱ型公式。這是歸結(jié)證明的一個(gè)重要思想，即要證明命題A，只要證明

不可滿足(反證法的運(yùn)用)；要證明

的不可滿足，只要證明

的子句集的不可滿足；而要證明

的子句集的不可滿足，只要證明

的Herbrand域的不可滿足。

Skolem標(biāo)準(zhǔn)范式

定義2

以前束范式中消去全部存在量詞所得到的公式即為

斯柯林(Skolem)標(biāo)準(zhǔn)

范式。

例如，如果用Skolem函數(shù)

代替前束范式

中的y即得到Skolem標(biāo)準(zhǔn)范式:

Skolem標(biāo)準(zhǔn)型的一般形式是

其中，

是一個(gè)合取范式，稱為

Skolem標(biāo)準(zhǔn)型的母式

。

將謂詞公式G化為Skolem標(biāo)準(zhǔn)型的步驟如下：

(1) 消去謂詞公式G中的蘊(yùn)涵(→) 和雙條件符號(?)，以

代替

以

代替

。

(2) 減小否定符號(

) 的轄域，使否定符號“

”最多只作用到一個(gè)謂詞上。

(3) 重新命名變元名，使所有的變元的名字均不同，并且自由變元及約束變元亦不同。

(4) 消去存在量詞。這里分兩種情況，一種情況是存在量詞不出現(xiàn)在全稱量詞的轄域內(nèi)，此時(shí)，只要用一個(gè)新的個(gè)體常量替換該存在量詞約束的變元，就可以消去存在量詞；另一種情況是存在量詞位于一個(gè)或多個(gè)全稱量詞的轄域內(nèi)，這時(shí)需要用一個(gè)Skolem函數(shù)替換存在量詞而將其消去。

(5) 把全稱量詞全部移到公式的左邊，并使每個(gè)量詞的轄域包括這個(gè)量詞后面公式的整個(gè)部分。

(6) 母式化為合取范式：任何母式都可以寫成由一些謂詞公式和謂詞公式否定的析取的有限集組成的合取。

需要指出的是，由于在化解過程中，消去存在量詞時(shí)作了一些替換，一般情況下，公式G的Skolem標(biāo)準(zhǔn)型與G 并不等值。

例1

，消去存在量詞后得

，若論域是

，取D下的一個(gè)解釋

：

，顯然G與

不等價(jià)。

Skolem函數(shù)

定義3

如果存在量詞在全稱量詞的轄域內(nèi)，如公式

，變量x的取值依賴于變量y的取值，令這種依賴關(guān)系由函數(shù)

來表示，它把每個(gè)y值映像到存在的那個(gè)x，這個(gè)函數(shù)稱為

斯柯林(Skolem)函數(shù)

。

如果用Skolem函數(shù)代替存在的個(gè)體，就可以消去存在量詞。注意，這里的函數(shù)

應(yīng)是原合式公式中沒有的符號。公式

可化為

。