斯科倫範式

如果一階邏輯式的前束範式只有全稱量詞，則稱其為是符合Skolem 範式的。一個公式可以被Skolem 化，就是說消除它的存在量詞並生成最初的公式的等價可滿足的公式。Skolem 化是如下二階邏輯的等價應用：

$\forall x\exists yR(x,y)\Leftrightarrow \forall xR(x,f(x))$

Skolem 化的本質是對如下形式的公式的觀察

$\forall x_{1}\dots \forall x_{n}\exists yR(x_{1},\dots ,x_{n},y)$

它在某個模型中是可滿足的，在這個模型必定對於所有的

$x_{1},\dots ,x_{n}$

有某些點$y$ 使得

$R(x_{1},\dots ,x_{n},y)$

為真，並且必定存在某個函數(選擇函數)

$y=f(x_{1},\dots ,x_{n})$

使得公式

$\forall x_{1}\dots \forall x_{n}R(x_{1},\dots ,x_{n},f(x_{1},\dots ,x_{n}))$

為真。函數 f 叫做 Skolem 函數。

舉例說明:

$\exists x\forall yR(x,y)\Rightarrow \forall yR(a,y)$ 其中a為常數

$\forall x\exists yR(x,y)\Leftrightarrow \forall xR(x,f(x))$

$\forall x\forall y\exists zR(x,y,z)\Leftrightarrow \forall x\forall yR(x,y,f(x,y))$

在一階邏輯中為何我們需要Skolem範式?

首先當我們根據一階邏輯構成法則構建一個公式，為了測試證明是否該公式存在一個模型（或解釋），也就是說他是否是可滿足的

• 所謂可滿足式的公式是指該公式至少擁有一個模型(或稱解釋)，使該公式為真(也就是說使該公式在一定的解釋下有意義)

為了能夠測試證明所有公式的滿足性問題，我們就使用一種通過讓公式變形達到公式統一標準為目的的方法，來證明公式的滿足性問題 因此我們引入(Clause)句子的概念，也就是說把公式φ變形成Clause(φ)的形式來判斷公式φ的可滿足性問題

• 為何要把公式統一化？其目的是為了更好地使判斷可滿足性的算法應用於任何公式中，因此公式變形成統一的表達標準

我們有一個定理: 如果φ是可滿足的當且僅當Clause(φ)是可滿足性的

由於該定理的存在，確保公式的可滿足性在Clause(φ)中是等價的，所以我們應用算法，來使公式變形 在公式φ轉變成Clause(φ)過程中，由於根據公式構成規則，公式φ中可能有存在量詞∃，所以我們使用Skolemisation方法，其目的是消減公式φ中所有的存在量詞∃ 根據(Clause)句子的定義，句子中的每個變量必須是以所有量詞∀限定的約束變量

• 我們有一個定理: 前提如果有公式φ且φ是(formule normale negative)否定標準式，如果公式ψ是由公式φ通過Skolemisation方法所得到公式，那麼
  • 如果 I |= ψ ,那麼 I |= φ
  • 如果 I |= φ ,那麼存在I的保守擴展J J|= ψ

根據如上定理我們確保在使用Skolemisation方法後，公式φ和公式ψ的可滿足性是等價的

在應用Skolemisation方法之前，公式φ必須是(formule normale negative)否定標準式，否則可滿足性就有問題

比如有公式φ：

φ=˥(∃xp(x))∧(∃xp(x))

φ不是(formule normale negative)否定標準式，我們如果不把φ變成(formule normale negative)否定標準式，當我們應用Skolemisation方法後˥(∃xp(x))∧(∃xp(x))就變成˥p(a)∧p(b),a,b是常數，因此˥p(a)∧p(b)是可滿足式的，然而當我們先把φ轉換成(formule normale negative)否定標準式，

於是˥(∃xp(x))∧(∃xp(x))就變成∀x˥p(x)∧(∃xp(x)),我們應用Skolemisation方法以後就變成∀x˥p(x)∧p(a),a為常數，此時∀x˥p(x)∧p(a)為永假式，所以當應用Skolemisation方法前，公式必須是(formule normale negative)否定標準式

參見

• 歸結原理

外部連結

• Skolemization on PlanetMath.org （頁面存檔備份，存於網際網路檔案館）