Skolem标准型是Skolem于1920年提出的一个使一阶公式标准化的方法，其定义如下：Skolem标准型是如下任意一种形式的一阶命题：(1)∀x1∀x2...∀xm∃y1∃y2...∃ynUx1x2...xmy1y2...yn(∏Σ型 )；(2)∀x1∀x2...∀xmUx1x2...xm(∏型)；(3)∃x1∃x2...∃xmUx1x2...xm(Σ型)。其中，U是不包含量词且连接符仅仅为∧，∨，→的公式。

外文名

Skolemstandardmodel

所属学科

数学

基本介绍

定义1

Skolem标准型是如下任意一种形式的一阶命题：

(∏∑型)

（1）

(∏或∑型 )

(2)

(∏型)

(3)

(∑型)

其中，U是不包含量词且连接符仅仅为

的公式。

第(1)种标准型显然借鉴了亚里士多德三段论的直言命题的形式。第(1)、(3) 种标准型中的

是可以消除的。消除的方法有三种。第一种是将公式中的

换为

，然后对于原来

的约束项变为它前面的变量确定的新的变量，这样原来的公式成为仅由全称量词约束的公式，原来的存在量词约束的项的解释缩小为由它前面的项所确定的量

。如

转换为

，也可写成

。如果有明确的y的解释域，这种转换后新的公式没有改变与原有公式的真假值的等价性；否则真假值的等价性可能有变。第二种是将(1)公式中的

换为

，然后对于对U增加解释性的关系，使得公式对于原来公式的域中不能满足的

的项增补一个非关系，进而扩大了y 的解释域。第三种是将公式中的

去掉，然后对于原来的约束项变为一个确定的解释域中的项a，原有公式的真假值的等价性遭到破坏，但是在确定公式的无效性(永假) 时，改变后的公式与原公式具有同等意义。无论哪种方法都可以消除存在量词

。用上述同样的方法，显然，也可以将一阶公式转换为标准型(注意转变后其有效性可能与原公式并不完全等价)。

总之，对于一阶命题(公式)的Skolem 标准化，是基于

Skolem 标准化的定理

：对于任何一阶命题A，都存在一个标准型命题

，使得当

是可满足的，A在其解释域是可满足的。

定理1

一阶公式G 与G的子句集S并不相等，但是它们具有相同的不可满足性。

证明:

如果公式G 是∏型，解释G 的域

，这与子句集解释S的域完全重合。同时，G 不能满足，也就意味着

中至少有一个子句不能满足，此时

为0；由于

，此时S也为0，即Ⅱ型的不可满足性与子句集S的不可满足性完全相同。

如果公式G 是∏∑型或∑型，此时G将有

约束的项

，如果子句集中对于

的解释域设置为

将与

的解释域可能不一致。但是，对于不可满足性而言，“没有任何一个解释满足G 中

构成的公式”和“

均不可满足S中

构成的公式”在逻辑上是一致的。可参照直言命题量词的否定运算规则，即

，它是说，“不存在”(即的不可满足性) 意味着“

”所描述的(与

约束的项的)域“全都不”满足。“

”是表述在G中：而“

”表述在子句集中——因为子句不再表示量词约束意味着以项的全称为解释域，

恰好表达了所有解释的不满足性。

定理1的启示在于，对于∏∑型或∑型的一阶公式，如果证明其不可满足性，可以证明其替换

之后形成的Ⅱ型公式。这是归结证明的一个重要思想，即要证明命题A，只要证明

不可满足(反证法的运用)；要证明

的不可满足，只要证明

的子句集的不可满足；而要证明

的子句集的不可满足，只要证明

的Herbrand域的不可满足。

Skolem标准范式

定义2

以前束范式中消去全部存在量词所得到的公式即为

斯柯林(Skolem)标准

范式。

例如，如果用Skolem函数

代替前束范式

中的y即得到Skolem标准范式:

Skolem标准型的一般形式是

其中，

是一个合取范式，称为

Skolem标准型的母式

。

将谓词公式G化为Skolem标准型的步骤如下：

(1) 消去谓词公式G中的蕴涵(→) 和双条件符号(↔)，以

代替

以

代替

。

(2) 减小否定符号(

) 的辖域，使否定符号“

”最多只作用到一个谓词上。

(3) 重新命名变元名，使所有的变元的名字均不同，并且自由变元及约束变元亦不同。

(4) 消去存在量词。这里分两种情况，一种情况是存在量词不出现在全称量词的辖域内，此时，只要用一个新的个体常量替换该存在量词约束的变元，就可以消去存在量词；另一种情况是存在量词位于一个或多个全称量词的辖域内，这时需要用一个Skolem函数替换存在量词而将其消去。

(5) 把全称量词全部移到公式的左边，并使每个量词的辖域包括这个量词后面公式的整个部分。

(6) 母式化为合取范式：任何母式都可以写成由一些谓词公式和谓词公式否定的析取的有限集组成的合取。

需要指出的是，由于在化解过程中，消去存在量词时作了一些替换，一般情况下，公式G的Skolem标准型与G 并不等值。

例1

，消去存在量词后得

，若论域是

，取D下的一个解释

：

，显然G与

不等价。

Skolem函数

定义3

如果存在量词在全称量词的辖域内，如公式

，变量x的取值依赖于变量y的取值，令这种依赖关系由函数

来表示，它把每个y值映像到存在的那个x，这个函数称为

斯柯林(Skolem)函数

。

如果用Skolem函数代替存在的个体，就可以消去存在量词。注意，这里的函数

应是原合式公式中没有的符号。公式

可化为

。