Skolem标准型 gaunthan Posted on Nov 12 2016 ? Discrete Mathematics ? > **Skolem标准型**就是将谓词逻辑公式中的全称量词和存在量词所管辖的变量映射到Skolem函数或无参Skolem变量(常量),形成的公式。 ## 前束范式 Skolem标准型是在前束范式的基础上进行变量映射的。**前束范式**的定义如下: > A是一个前束范式,如果A中的一切量词都位于该公式的最左边(不含否定词),且这些量词的辖域都延伸到公式的末端。 将谓词公式化为前束范式的过程经常会用到**改名规则**和**量词辖域扩张和收缩定律**。 ## Skolem标准型 ### 定义 前束范式中消去所有的量词,则称这种形式的谓词公式为**Skolem标准型**,任何一个谓词公式都可以化为与之对应的Skolem标准型。但是,Skolem标准型可以不唯一。 ### 转化过程 Skolem标准型的转化过程为: 1. 依据约束变量换名规则,首先将公式变型为前束范式; 2. 依照量词消去原则消去或者略去所有量词。 由前束范式的定义可知,前束范式最左端的所有量词的辖域延伸到整个谓词公式的结尾。此时如果某个存在量词: - 在其他全称量词的辖域范围之内,则存在某种依赖关系。例如,$ (\forall x)(( \exists y)(P(x, y)))$可以表示“每一个人$x$都有自己的$y$年龄,那么显然,年龄$y$与人$x$有关。可以用一个函数$f(x)$描述这种依赖关系,$f(x)$把每一个$x$值映射为存在的$y$值。这样的函数叫**Skolem函数**。 - 不在任何全称量词的辖域范围之内,可以将变量映射为一个常量,该常量也可以认为是没有变量的Skolem函数。如$(\exists x)P(x)$,成为$P(a)$,其中$a$为没有在谓词公式中出现过的任意常数。 经过上述转换过程的谓词公式称为Skolem标准型。具体的**量词消去原则**为: > - 消去存在量词“$\exists$”,即,将该量词约束的变量用任意常量($a, b$等)或任意变量的函数($f(x), g(y)$等)代替。如果存在量词左边没有任何全称量词,则只将其改写成为常量;如果左边有全称量词,消去时该变量改写为全称量词的函数。 > - 略去全称量词“$\forall$”,简单地省略掉该量词。 ### 一个例子 比如现在要将下面的前束范式转为Skolem标准型: $$(\forall x)(\exists y)(\exists u)(\forall v)( P(a, x, y) \lor Q(v, b) \lor R(u) )$$ 则其转换过程为: - 消去$(\exists y)$。因为它左边只有$(\forall x)$,所以使用$x$的函数$f(x)$代替之,得公式为: $$(\forall x)(\exists u)(\forall v)( P(a, x, f(x)) \lor Q(v, b) \lor R(u) )$$ - 消去$(\exists u)$,同理使用$g(x)$代替之,得公式为: $$(\forall x)(\forall v)( P(a, x, f(x)) \lor Q(v, b) \lor R(g(x)) )$$ - 省略所有全称量词,得公式为: $$P(a, x, f(x)) \lor (Q(v, b) \lor R(g(x))$$ ### Skolem定理 > 任意谓词公式$G$的Skolem标准型同$G$并不等值。 赏 Wechat Pay Alipay 一阶谓词逻辑归结原理 Markdown说明