斯科伦范式, 如果一阶逻辑式的前束范式只有全称量词, 则称其为是符合skolem, 范式的, 一个公式可以被skolem, 就是说消除它的存在量词并生成最初的公式的等价可满足的公式, skolem, 化是如下二阶逻辑的等价应用, displaystyle, forall, exists, leftrightarrow, forall, skolem, 化的本质是对如下形式的公式的观察, displaystyle, forall, dots, forall, exists, dots, 它在某个模型中是可满足的, 在. 如果一阶逻辑式的前束范式只有全称量词 则称其为是符合Skolem 范式的 一个公式可以被Skolem 化 就是说消除它的存在量词并生成最初的公式的等价可满足的公式 Skolem 化是如下二阶逻辑的等价应用 x y R x y x R x f x displaystyle forall x exists yR x y Leftrightarrow forall xR x f x Skolem 化的本质是对如下形式的公式的观察 x 1 x n y R x 1 x n y displaystyle forall x 1 dots forall x n exists yR x 1 dots x n y 它在某个模型中是可满足的 在这个模型必定对于所有的 x 1 x n displaystyle x 1 dots x n 有某些点y displaystyle y 使得 R x 1 x n y displaystyle R x 1 dots x n y 为真 并且必定存在某个函数 选择函数 y f x 1 x n displaystyle y f x 1 dots x n 使得公式 x 1 x n R x 1 x n f x 1 x n displaystyle forall x 1 dots forall x n R x 1 dots x n f x 1 dots x n 为真 函数 f 叫做 Skolem 函数 举例说明 x y R x y y R a y displaystyle exists x forall yR x y Rightarrow forall yR a y 其中a为常数 x y R x y x R x f x displaystyle forall x exists yR x y Leftrightarrow forall xR x f x x y z R x y z x y R x y f x y displaystyle forall x forall y exists zR x y z Leftrightarrow forall x forall yR x y f x y 在一阶逻辑中为何我们需要Skolem范式 编辑首先当我们根据一阶逻辑构成法则构建一个公式 为了测试证明是否该公式存在一个模型 或解释 也就是说他是否是可满足的 所谓可满足式的公式是指该公式至少拥有一个模型 或称解释 使该公式为真 也就是说使该公式在一定的解释下有意义 为了能够测试证明所有公式的满足性问题 我们就使用一种通过让公式变形达到公式统一标准为目的的方法 来证明公式的满足性问题 因此我们引入 Clause 句子的概念 也就是说把公式f变形成Clause f 的形式来判断公式f的可满足性问题 为何要把公式统一化 其目的是为了更好地使判断可满足性的算法应用于任何公式中 因此公式变形成统一的表达标准我们有一个定理 如果f是可满足的当且仅当Clause f 是可满足性的由于该定理的存在 确保公式的可满足性在Clause f 中是等价的 所以我们应用算法 来使公式变形 在公式f转变成Clause f 过程中 由于根据公式构成规则 公式f中可能有存在量词 所以我们使用Skolemisation方法 其目的是消减公式f中所有的存在量词 根据 Clause 句子的定义 句子中的每个变量必须是以所有量词 限定的约束变量 我们有一个定理 前提如果有公式f且f是 formule normale negative 否定标准式 如果公式ps是由公式f通过Skolemisation方法所得到公式 那么 如果 I ps 那么 I f 如果 I f 那么存在I的保守扩展J J ps根据如上定理我们确保在使用Skolemisation方法后 公式f和公式ps的可满足性是等价的在应用Skolemisation方法之前 公式f必须是 formule normale negative 否定标准式 否则可满足性就有问题比如有公式f f xp x xp x f不是 formule normale negative 否定标准式 我们如果不把f变成 formule normale negative 否定标准式 当我们应用Skolemisation方法后 xp x xp x 就变成 p a p b a b是常数 因此 p a p b 是可满足式的 然而当我们先把f转换成 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 页面存档备份 存于互联网档案馆 取自 https zh wikipedia org w index php title 斯科伦范式 amp oldid 67705578, 维基百科，wiki，书籍，书籍，图书馆，
