查看“︁斯科伦范式”︁的源代码

{{Cleanup rewrite|time=2024-06-19T12:00:38+00:00}}
如果[[一阶逻辑]]式的[[前束范式]]只有全称量词，则称其为是符合'''Skolem 范式'''的。一个公式可以被'''Skolem 化'''，就是说消除它的存在量词并生成最初的公式的[[等价可满足]]的公式。Skolem 化是如下[[二阶逻辑]]的等价应用：

:<math>\forall x \exists y R(x,y) \Leftrightarrow\forall x R(x,f(x))</math> 

Skolem 化的本质是对如下形式的公式的观察

:<math>\forall x_1 \dots \forall x_n \exists y R(x_1,\dots,x_n,y)</math> 

它在某个[[模型论|模型]]中是可满足的，在这个模型必定对于所有的

:<math>x_1,\dots,x_n</math> 

有某些点<math>y</math> 使得 

:<math>R(x_1,\dots,x_n,y)</math> 

为真，并且必定存在某个函数([[选择公理|选择函数]])

:<math>y = f(x_1,\dots,x_n)</math> 

使得公式

:<math>\forall x_1 \dots \forall x_n R(x_1,\dots,x_n,f(x_1,\dots,x_n))</math> 

为真。函数 ''f'' 叫做 '''Skolem 函数'''。

举例说明:
:<math>\exists x \forall y R(x,y)  \Rightarrow\forall y R(a,y)</math> 其中a为常数
:<math>\forall x \exists y R(x,y) \Leftrightarrow\forall x R(x,f(x))</math> 
:<math>\forall x \forall y \exists z R(x,y,z) \Leftrightarrow\forall x \forall y R(x,y,f(x,y))</math>

== 在一阶逻辑中为何我们需要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)否定标准式

== 参见 ==
*[[归结原理]]

== 外部链接 ==
* [http://planetmath.org/encyclopedia/Skolemization.html Skolemization on PlanetMath.org] {{Wayback|url=http://planetmath.org/encyclopedia/Skolemization.html |date=20060227172153 }}

[[Category:模型论]]
[[Category:数学公式]]