斯科伦范式

维基百科,自由的百科全书
跳转至: 导航搜索

一阶逻辑公式Skolem 范式的,如果它的前束范式只有全称量词。一个公式可以被Skolem 化,就是说消除它的存在量词并生成最初的公式的等价可满足的公式。Skolem 化是如下(二阶的)等价的应用

\forall x \exists y R(x,y) \Leftrightarrow\forall x R(x,f(x))

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

\forall x_1 \dots \forall x_n \exists y R(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 y R(x,y)  \Rightarrow\forall y R(a,y) 其中a为常数
\forall x \exists y R(x,y) \Leftrightarrow\forall x R(x,f(x))
\forall x \forall y \exists z R(x,y,z) \Leftrightarrow\forall x \forall y R(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)否定标准式

参见[编辑]

外部链接[编辑]