量词实例化

定义置换就是用一个变量替换另一个变量，如

\theta=\{a/b\}

是说这个置换的名字叫 $\theta$ ，它将语句中的变量 $a$ 都换成变量 $b$ 。应用一个变换可以这样表示

SUBSET(\theta,\alpha)

表示对语句 $\alpha$ 应用置换 $\theta$

全称量词实例化可以用任意的变量置换全称量化的变量，如对于

\forall x \, (King(x) \land Greedy(x) \Rightarrow Evil(x))

令置换 $\theta = \{x / John\}$ ，可得到

King(John) \land Greedy(John) \Rightarrow Evil(John)

存在量词实例化同样使用置换，不过置换的变量应当是从未出现的，称为斯科伦常量，如

\exists x \, (Crown(x) \land OnHead(x, John))

可得

Crown(C_1) \land OnHead(C_1, John)

其中 $C_1$ 是斯科伦常量，它从未出现过。在进行实例化后，得到的语句应取代原先的语句，意为存在量词实例化只能进行一次。但是全称量词可以多次实例化，可以获得多种不同的结果

量词约简为命题推断

量词的约简分为两步

对全称量词的语句，枚举所有的对象进行实例化
对存在量词的语句，用斯科伦常量进行一次实例化

不过此处会出现问题，函数作用与对象上会得到对象，它还能再被函数作用一次得到新的对象。这回陷入无限的嵌套中

对于该问题有Herbrand定理

Note

如果有限的一阶语句蕴含某个语句 $\alpha$ ，则一定存在有限步的推导。即将这些一阶语句命题化后存在一个有限嵌套深度的子集可以完成证明

这说明一阶逻辑的蕴含问题是半可判定的，也就是说存在有限步内能判断语句成立，却不能判断语句不成立

不过即便不考虑函数，对于 $n$ 个对象和一个 $k$ 元谓词，实例化的复杂度也是指数级的

n^k

其中有大量无关的语句。为了只实例化需要的实例，需要引入一般化肯定前件（GMP）

一般化肯定前件

对于 $n$ 个原子语句 $p_1,p_2,\cdots,p_n$ 和 $1$ 个蕴含语句，更准确来说应该是一阶确定子句，只有一个正文字

p_1'\land p_2'\land\cdots\land p_n'\Rightarrow q

如果能找到一个置换 $\theta$ 使得对应语句相同

SUBSET(\theta,p_i)=SUBSET(\theta,p_1')

注意等值表示的是相同而不是逻辑上的相等。那么给定前件为 $p_1',p_2',\cdots,p_n'$ 的该蕴含语句

p_1',p_2',\cdots,p_n',(p_1'\land p_2'\land\cdots\land p_n'\Rightarrow q)

可以被替换为结论的置换

SUBSET(\theta,q)

一个简单的例子是

\forall x \, (King(x) \land Greedy(x) \Rightarrow Evil(x))\\ King(John)\\ \forall y \, Greedy(y)\\ Brother(John, Richard)

由于取置换

\theta = \{x/John, y/John\}

各语句被置换后有

Subst(\theta, p_1') = Subst(\theta, p_1) = King(John)

Subst(\theta, p_2') = Subst(\theta, p_2) = Greedy(John)

那么原来的蕴含语句 $Subst(\theta, q)$ 就应被实例化为

Evil(John)

没有多余的实例化

GMP的核心在于那个置换，称为合一子。两个语句的合一子可能不止一种，但是会存在一个最一般的合一子，其他所有的何意子都可以在其基础上再施加置换得到，称为最一般合一子MGU

不过使用GMP的条件是所有的变量假设均为全称量词，并且只能作用于一阶确定子句。在这个条件下，GMP是可靠且完备的

一阶逻辑的归结

一阶逻辑转换为合取范式

要对一阶逻辑使用归结，应当先将一阶逻辑语句转换为合取范式CNF。要将语句转化为CNF，应当先消去蕴含，利用逻辑等值式

A\Rightarrow B\equiv \neg A\lor B

使用时需要注意，虽然需要对 $\forall,\exists$ 取反，但是内层的 $\Rightarrow$ 取反时不应影响外层的量词，如

\forall x [\forall y \, Animal(y) \Rightarrow Loves(x, y)] \Rightarrow [\exists y \, Loves(y, x)]

\rightarrow \forall x\neg [\forall y \neg Animal(y) \lor Loves(x, y) \lor (\exists y \, Loves(y, x))]

其中 $\forall x$ 是外层的量词，作用于蕴含的两端，不受取反影响；而蕴含的前提中 $\exists y$ 不作用于结论，应当取反

第二步是将非号移到量词作用域的内部，形成一系列由与和或连接的原子语句，如

\forall x\neg [\forall y \neg Animal(y) \lor Loves(x, y) \lor (\exists y \, Loves(y, x))]

\rightarrow \forall x \, [\exists y \, Animal(y) \land \neg Loves(x, y) \lor (\exists y \, Loves(y, x))]

第三步是变量标准化，不同语句间如果不是同一个对象应使用不同的名字，虽然量词的修饰允许，但为了后续步骤还是需要这样做，如此处将蕴含结论的 $y$ 换为了另一个名称 $z$

\forall x \, [\exists y \, Animal(y) \land \neg Loves(x, y) \lor (\exists y \, Loves(y, x))]

\rightarrow \forall x \, [\exists y \, Animal(y) \land \neg Loves(x, y) \lor \exists z \, Loves(z, x)]

第四步是将存在量词实例化。需要注意的是，此处实例化并不是化为斯科伦常量，而是斯科伦函数。它是所有基本对象的函数，代表未知的确定函数，这是因为斯科伦常量太过一般，至少斯科伦函数能提供自变量的信息。如

\forall x \, [\exists y \, Animal(y) \land \neg Loves(x, y) \lor \exists z \, Loves(z, x)]

\rightarrow \forall x \, [Animal(F(x)) \land \neg Loves(x, F(x)) \lor Loves(G(x), x)]

不一样的变量应替换为不一样的斯科伦函数

最后将全称量词去除，因为斯科伦函数可以是所有基本对象的任意函数，本身就是对所有基本对象的实例化。上面的例子中，最后将得到语句

Animal(F(x)) \land \neg Loves(x, F(x)) \lor Loves(G(x), x)

不过为了得到CNF的形式，还需将其转为合取

[Animal(F(x)) \lor Loves(G(x), x)] \land [\neg Loves(x, F(x)) \lor Loves(G(x), x)]

一阶逻辑的归结规则

Note

对于两个一阶逻辑的CNF语句，若其中各有一个文字，在某种置换规则 $\theta$ 作用下互为反文字，则这两个文字可以被消去

具体来说，对于一阶逻辑语句

a_0\land a_1\land a_2\land\cdots\land a_n

b_0\land b_1\land b_2\land\cdots\land b_m

若存在一个置换规则使得 $\theta$ 使得

SUBSET(\theta,b_0)=\neg a_0

则它们两个等价于