斯科伦范式

如果一阶逻辑式的前束范式只有全称量词，则称其为是符合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 （页面存档备份，存于互联网档案馆）