斯科伦范式

易经学习

天地变化的道理

分类目录

使用率很高网站

文章列表

生活要常常分享

维基百科

您身边百科全书

产品秀秀

免费为您秀产品

斯科伦范式

点击查看词条快照

如果一阶逻辑式的前束范式只有全称量词，则称其为是符合Skolem 范式的。一个公式可以被Skolem 化，就是说消除它的存在量词并生成最初的公式的等价可满足的公式。Skolem 化是如下二阶逻辑的等价应用： formula_1 Skolem 化的本质是对如下形式的公式的观察 formula_2 它在某个模型中是可满足的，在这个模型必定对于所有的 formula_3 有某些点formula_4 使得 formula_5 为真，并且必定存在某个函数(选择函数) formula_6 使得公式 formula_7 为真。函数 "f" 叫做 Skolem 函数。举例说明: formula_8 其中a为常数 formula_1 formula_10 在一阶逻辑中为何我们需要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)否定标准式

地税

包叙定

波斯尼亚地区

物业税

阿迪格语

约翰三世 (布列塔尼)

哈库其阿迪格语

瑞典克朗

捷星亚洲航空

车臣语

印古什语

约翰三世