1. 带有量词的自然演绎推理系统结论备忘
$$
\neg (\exist x)P\Leftrightarrow (\forall x)(\neg P)
$$
$$
\neg(\forall x)P\Leftrightarrow(\exist x)(\neg P)
$$
$$
(\forall x)(P\wedge Q)\Leftrightarrow(\forall x)P\wedge(\forall x)Q
$$
$$
(\exist x)(P\vee Q)\Leftrightarrow(\exist x)P\vee(\exist x)Q
$$
2. 谓词公式的置换和合一
置换的概念
置换是形如：
$$
\theta={t_1/x_1, t_2/x_2, \cdots,t_n/x_n}
$$
的有限集合，其中$t_i$是谓词中的项，$x_i$是互不相同的变量，$t_i/x_i$表示用前者替换后者。要求：$t_i\neq x_i$。
置换的合成
设：
$$
\theta={t_1/x_1, t_2/x_2, \cdots,t_n/x_n},\lambda={u_1/y_1,u_2/y_2,\cdots,u_n/y_n}
$$
是两个置换，则将集合：
$$
\gamma={t_1\lambda/x_1,t_2\lambda/x_2,\cdots,u_1/y_1,u_2/y_2,\cdots,u_n/y_n}
$$
中符合下列条件的元素删除：
- $t_i\lambda/x_i$，其中$t_i\lambda=x_i$。
- $u_i/y_i$，其中$y_i\in {x_1,x_2,\cdots,x_n}$。
如此得到的集合$\gamma$是一个置换，且：
$$
\gamma=\theta·\lambda
$$
什么意思？首先将$\lambda$置换应用到$\theta$置换上，$t_i\lambda/x_i$的意思是说，先使用$\lambda$变换替换$t_i$，再应用$\theta$本身的替换方法，使用$x_i$替换$t_i\lambda$。对于有些变元，在$\theta$变换中未被替换，就需要把一些在$\lambda$变换中出现的规则添加到集合中，最后去重，则得到合成的集合。
举个例子，求下面两个置换的合成：
$$
\theta={b/y,c/z},\lambda={x/a,y/b}
$$
得到集合：
$$
\gamma={b\lambda/y,c\lambda/z,x/a,y/b}
$$
其中：
$$
b\lambda=y
$$
集合变化成：
$$
\gamma={y/y,c/z,x/a,y/b}
$$
去重：
$$
\gamma={c/z,x/a,y/b}
$$
合一的概念
设有公式集：
$$
F={F_1,F_2,\cdots,F_n}
$$
若存在一个置换$\theta$，令：
$$
F_1\theta=F_2\theta=\cdots=F_n\theta
$$
则称$\theta$为$F$的一个合一。
最一般合一
设$\sigma$是$F$的一个合一，若对$F$的任何一个合一$\theta$都存在一个置换$\lambda$，令$\theta=\sigma·\lambda$，则称$\sigma$是一个最一般合一(most general unifier)，简记为mgu。
3. 归结演绎推理
通过某些方法，可以简化表达式。
前束范式
所有量词均非否定地出现在公式最前面，且辖域为整个公式。
比如：
$$
(\forall x)(\forall y)(P(x)\vee Q(y)\vee R(x, y))
$$
化简方法
在谓词逻辑中，任何一个谓词公式都可以通过推理规则化简。
1. 消去推导义连接词
通过应用：
$$
P\to Q\Leftrightarrow \neg P\vee Q
$$
$$
P\leftrightarrow Q\Leftrightarrow (P\wedge Q)\vee(\neg P\wedge\neg Q)
$$
可消去谓词公式中的$\to$和$\leftrightarrow$两个连接词。
对于公式:
$$
(\forall x)((\forall y)P(x,y)\to\neg(\forall y)(Q(x,y)\to R(x,y)))
$$
可化简为：
$$
(\forall x)(\neg(\forall y)P(x,y)\vee \neg(\forall y)(\neg Q(x,y)\vee R(x,y)))
$$
2. 减少否定符号的辖域
通过应用带有量词的自然演绎推理系统结论和摩根定律，可令否定词$\neg$的辖域最多只作用于一个谓词上。
上面的公式可以化简为：
$$
(\forall x)((\exist y)\neg P(x,y)\vee(\exist y)(Q(x,y)\wedge\neg R(x,y)))
$$
3. 标准化变元
让变元的名字尽可能不同。
上面的公式可以化简为：
$$
(\forall x)((\exist y)\neg P(x,y)\vee(\exist z)(Q(x,z)\wedge\neg R(x,z)))
$$
4. 化为前束范式
因为我们将变元标准化了，所以可以把量词移动到最前面。
上面的公式可以化简为：
$$
(\forall x)(\exist y)(\exist z)(\neg P(x,y)\vee (Q(x,z)\wedge R(x,z)))
$$
5. 消除存在量词
消去存在量词时，需要区分以下两种情况：
- 若存在量词不出现在全称量词的辖域内（即它的左边没有全称量词），只要用一个新的个体常量替换受该存在量词约束的变元，就可消去该存在量词。
- 若存在量词位于一个或多个全称量词的辖域内，则需要用到Skolem函数。
Skolem函数为：
$$
(\forall x)(\forall y)(\exist z)(P(x,y, z))\Leftrightarrow \forall xP(x, y, f(x,y))
$$
上面的公式可以化简为：
$$
(\forall x)(\neg P(x, f(x))\vee (Q(x, g(x))\wedge \neg R(x, g(x))))
$$
6. 化为Skolem标准型
应用如下关系：
$$
P\vee(Q\wedge R)\Leftrightarrow (P\vee Q)\wedge(P \vee R)
$$
上面的公式可以化简为：
$$
(\forall x)(\neg P(x, f(x))\vee (Q(x, g(x))\wedge (\neg P(x, f(x))\wedge \neg R(x, g(x))))
$$
7. 消除全称量词
直接省略全称量词即可。
上面的公式可以化简为：
$$
\neg P(x, f(x))\vee (Q(x, g(x))\wedge (\neg P(x, f(x))\wedge \neg R(x, g(x)))
$$
8. 消除合取词
将前束范式拆成一系列子句。以合取词$\wedge$为分割。
上面的公式可以拆分为：
$$
\neg P(x,f(x))\vee Q(x,g(x))
$$
$$
\neg P(x,f(x))\vee\neg R(x,g(x))
$$
9. 改变量名
令子句间，彼此没有共同变量。更改变量名，不会改变子句的真值。
上面的公式可以变为:
$$
\neg P(x,f(x))\vee Q(x,g(x))
$$
$$
\neg P(y,f(y))\vee\neg R(y,g(y))
$$
10. 通过子句的真值，判断原式的真值
子句之间是合取关系，子句集中若有一个子句不可满足，则子句集不可满足。此外，空子句也不可满足。
怎么判断？应用鲁滨逊归结原理。这个原理的思想很简单，归结时，删除句子中的互补源自谓词公式，即$\neg P $和$P$。
假设有三个子句：
$$
C_1 = \neg P \vee Q
$$
$$
C_2 = \neg Q
$$
$$
C_3 = P
$$
应用归结定理将他们归结起来得到的结果，就是原式子的结果。
先归结$C_1C_2$，得到$\neg P$，再和剩下的子句归结，得到空子句，不可满足。
这里也有几个重要的结论：设$C_1C_2$归结得到$C_{12}$，则有$C_{12}=C_1C_2$。