2.3 谓词逻辑
谓词逻辑的主要思想：世界是由对象组成的，可以由标识符和属性区分它们，并且它们存在相互之间的关系。
该部分是 离散数学 一阶逻辑 部分的内容，故略去。
如果谓词 $P$ 中的所有个体都是个体常量、变元或函数，则该谓词为一阶谓词。
如果某个个体本身又是一个一阶谓词，则称 $P$ 为二阶谓词，以此类推。
将公式 $A$ 在结构 $\mathcal U$ 及指派 $A$ 取值为真记为 $\vDash_U A[s]$，否则为 $\not \vDash_U A[s]$
2.4 归结推理
逻辑推理的三种形式：演绎推理、归纳推理、溯因推理
归结推理：证明 $P \to Q$ 等价于证明 $\boldsymbol F = (P_1 \land P_2 \land \cdots \land P_n) \land \lnot Q$ 为假，转换为证明 子句集 $\boldsymbol S = \{P_1, P_2, \cdots, P_n, Q\}$ 是不可满足的。
文字：原子公式及其否定
子句：任何文字的析取。
子句集：由子句构成的集合。
命题逻辑的归结推理
对于前提集 $F$ 和命题 $P$，将 $F$ 和 $\lnot P$ 写成子句集 $S = S_0 \cup S_{\lnot P}$，对其反复应用归结推理，直至导出空子句（False），说明找到矛盾，则证明结束。
谓词逻辑的归结推理
合一：寻找项之间合适的变量置换使得表达式一致。
变量到项的置换： $\sigma = \{t_1/v_1, t_2/v_2,\cdots,t_n/v_n\}$，$S$ 做 $\sigma$ 置换后记为 $S\sigma$
- $t_i/v_i$ 表示用 $t_i$ 替换 $v_i$，$t_i$ 是项，$v_i$ 是互不相同的变量
- $t_i \ne v_i$，$t_i$ 不能与 $v_i$ 有关，不允许置换本质上形成了环（包括自环）
- 变量到项的置换本质上是一种 一般到特殊 的过程。
合成置换：$(E\theta)\lambda = E(\theta\circ\lambda)$
- 若 $\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_m/y_m\}$
- 那么它们的复合为 $$\theta\circ \lambda = \{t_1\lambda/x_1, t_2\lambda/x_2, \cdots, t_n\lambda/x_n, ,u_1/y_1, u_2/y_2, \cdots, u_m/y_m\}$$
- 需要删去自环：$t_i\lambda /x_i = x_i / x_i$
- 需要删去第二次置换中变得无用的替换：$u_i/y_i,, y_i \in \{x_1,x_2,\cdots,x_n\}$
公式集的合一：对于 $F = \{F_1,F_2,\cdots,F_n\}$，若存在置换 $\lambda$ 使得 $F_1\lambda=F_2\lambda=\cdots=F_n\lambda$，则称公式集 $F$ 是合一的。
- 通常而言，使得公式集合一的置换是不唯一的。
- 使得公式集合一的置换可能不存在。
最一般合一（MGU）：对于 $F$ 的一个合一 $\sigma$，若对于其他合一 $\theta$，均 $\exists \lambda,, \theta = \sigma\circ\lambda$，则称 $\sigma$ 是 $F$ 的最一般合一。
- 如果可合一，那么一定就存在 MGU
- 最一般合一在变量重命名/等价代换意义下唯一。
MGU 的求解算法：对于 $F$，找出其差异集 $D$（两个公式在相同位置处不同符号的集合），并将其置换 $t_i/x_i$，并合并相同的表达式。
- 最终如果 $F$ 只有一个表达式，则算法终止，并且 $F$ 存在 MGU
- 最终如果 $F$ 仍有多个表达式且没法再置换，则算法终止，并且 $F$ 不存在 MGU，不可合一
在归结推理时，若 $C$ 有可合一的文字，那么在归结之前应当对这些文字进行合一。
二元归结式：对于两个没有相同变元的子句 $C_1,C_2$，若它们各自的一个文字 $L_1$ 和 $L_2$，若 $\sigma$ 是 $L_1$ 和 $L_2$ 的最一般合一，则它们的二元归结式为 $$C_{12} = (C_1\sigma - \{L_1\sigma\})\cup (C_2\sigma - \{L_2\sigma\})$$
对于一节谓词逻辑，归结推理是完备的。