归结法基本原理
归结法的基本原理是采用反证法（也称反演推理法）将待证明的表达式（定理）转换成为逻辑公式（谓词公式），然后再进行归结，归结能够顺利完成，证明原公式（定理）是正确的。
$def:$ $Q$ 为 $P_1,P_2, \cdots ,P_n$ 的逻辑结论，当且仅当 $P\wedge \neg Q$ 是不可满足的，结论才成立
这样做的原因是证明不可满足性要比证明可满足性简单得多。通俗来讲，若要证明定理：张三是个好人。可以反向证明定理：张三不是个好人那是不可能的。
用符号公式表示就是:
待证定理：$P \Rightarrow Q$
置换转换为普通谓词公式:再将其否定：$\neg(\neg P\vee Q) \Leftrightarrow P\wedge \neg Q$
即证明 $P\wedge \neg Q$ 为永假式
子句集
为了描述子句集，先给出如下几个名词的定义：
- 原子谓词公式：一个不能再分解的命题
- 文字：原子谓词公司及其否定
- $P$: 正文字
- $\neg P$: 负文字
- 子句：任何文字的析取式，任何文字本身也都是句子。
- 空子句：不包含任何文字的子句
- 子句集：所有子句的集合
例1： 将下列谓词公式化为子句集
A. 利用一下公式消去谓词公式中的$\rightarrow$ 和 $\leftrightarrow$ 符号
$P\rightarrow Q\Leftrightarrow \neg P\vee Q,P\leftrightarrow Q\Leftrightarrow (P\wedge Q)\vee (\neg P\wedge \neg Q)$
$\color{red}{\Longleftrightarrow} \forall x (\neg \forall yP(x,y) \vee \neg \forall y(\neg Q(x,y)\vee R(x,y)))$
B. 利用下列公式把否定符号 $\neg$ 移到紧靠谓词的位置上
双重否定律：$\neg (\neg P)\Leftrightarrow P$
摩根律：$\neg (p\wedge q)\Leftrightarrow \neg p\vee \neg q$
量词否定转换率：$\neg \exists xP\Leftrightarrow \forall x\neg P,\neg \forall xP\Leftrightarrow \exists x \neg P$
$\color{red}{\Longleftrightarrow} \forall x(\exists y\neg P(x,y)\vee \exists y(Q(x,y)\wedge \neg R(x,y)))$
C. 变量标准化(变元易名)
$\exists xP(x) = \exists yP(y),\forall xP(x) = \forall yP(y)$
$\color{red}{\Longleftrightarrow} \forall x(\exists y\neg P(x,y)\vee \exists \color{green}{z}(Q(x,\color{green}{z})\wedge \neg R(x,\color{green}{z})))$
D. 消去存在量词（两种情况）
$a.$ 存在量词不出现在全称量词的辖域内
$b.$ 存在量词出现在一个或者多个全称量词的辖域内
对于一般情况：
$\forall x_1(\forall x_2(\cdots \forall x_n(\exists yP(x_1,x_2,\cdots ,x_n,y)))\cdots)$
存在量词 $y$ 的Skolem函数为 $y=f(x_1,x_2,\cdots ,x_n)$
Skolem化：用Slolem函数代替每个存在量词化的变量的过程
如本例中两个存在量词 $y,z$ 只收到全称量词 $x$ 的约束，因此可以令：$y = f(x),z = g(x)$
$\color{red}{\Longleftrightarrow} \forall x(\neg P(x,\color{green}{f(x)})\vee (Q(x,\color{green}{g(x)})\wedge \neg R(x,\color{green}{g(x)})))$
E. 化为前束范式（本例中到此式子已经满足前束范式标准了）
$\color{red}{\Longleftrightarrow} \forall x(\neg P(x,\color{green}{f(x)})\vee (Q(x,\color{green}{g(x)})\wedge \neg R(x,\color{green}{g(x)})))$
F. 化为 $Skolem$ 标准型
$Skolem$ 标准型：
$M:$ 子句的合取式，称为Skolem标准型的母式，即去掉所有量词的前束范式。
利用分配律：
$p\vee(q\wedge r)\Leftrightarrow (p\vee q)\wedge (p\vee r)$
$p\wedge(q\vee r)\Leftrightarrow (p\wedge q)\vee (p\wedge r)$
$\color{red}{\Longleftrightarrow} \forall x((\neg P(x,\color{green}{f(x)})\vee Q(x,\color{green}{g(x)}))\wedge (\neg P(x,\color{green}{f(x)})\vee \neg R(x,\color{green}{g(x)})))$
G. 略去全称量词
$\color{red}{\Longleftrightarrow} ((\neg P(x,\color{green}{f(x)})\vee Q(x,\color{green}{g(x)}))\wedge (\neg P(x,\color{green}{f(x)})\vee \neg R(x,\color{green}{g(x)})))$
H. 消去合取词,成为一个子句集合（析取句的集合）
$\color{red}{\Longleftrightarrow} {(\neg P(x,\color{green}{f(x)})\vee Q(x,\color{green}{g(x)}), \neg P(x,\color{green}{f(x)})\vee \neg R(x,\color{green}{g(x)})}$
I. 子句变量的标准化（不同子句用不同变元）
$\color{red}{\Longleftrightarrow} {(\neg P(x,\color{green}{f(x)})\vee Q(x,\color{green}{g(x)}), \neg P(y,\color{green}{f(y)})\vee \neg R(y,\color{green}{g(y)})}$
鲁滨逊归结原理(判别子句集的不可满足性)
出发点：由于子句集当中的子句之间的关系是合取关系，因此只要有一个子句不可满足，则整个子句集就不可满足。
⭐️鲁滨逊归结原理的基本思想：
- 检查子句集 $S$ 中是否包含 空子句 ，若包含，则不可满足。
- 若不包含空子句，在 $S$ 中选择合适的子句进行归结，一旦归结出空子句，就说明 $S$ 是不可满足的。
- 另外需注意的是，对于鲁滨逊归结原理，如果在归结过程中出现空子句则可说明子句集的不可满足性；但若无法归结出空子句也无法说明该子句集可满足，也就是说鲁滨逊归结原理只能用来证伪。
命题逻辑中的归结原理：
$Def:$ 归结指的是，设$C_1$与$C_2$是子句集中的任意两个句子，如果$C_1$中的文字$L_1$与$C_2$中的文字$L_2$互补(同一谓词的正负文字)，那么从$C_1$与$C_2$中分别消去$L_1$和$L_2$, 并将两个子句中余下的部分 析取，构成一个新的子句 $C12$。
$Def:$ 归结式$C12$是其亲本子句$C_1$和$C_2$的逻辑结论。即如果$C_1$与$C_2$为真，则$C12$为真。
推论1： 由$C12$代替$C_1$和$C_2$后的新的子句集$S_1$的不可满足性也可代表原子句集的不可满足性（单向的）。
推论2： 若不作代替，直接将$C12$加入原子句集$S$得到新的子句集$S_2$,则$S$与$S_2$在不可满足的意义上是等价的（双向的）。
⭐️谓词逻辑中的归结原理：（含有变量的子句的归结）
谓词逻辑的归结比命题逻辑的归结要复杂得多，其中一个原因就是谓词逻辑公式中含有个体变量与函数。因此寻找互补的子句的过程就比较复杂。例如：
就不易从直接比较中发现这两个子句中含有的互补对，但如果将$x$取值为$a$,这很显然这两个句子中有互补对。
置换与合一：（对个体变量做适当替换）
置换： 将子句中的变量做适当替换，可替换成常量、变量、Skolem函数。
合一： 寻找相对变量的置换，使两个谓词公式一致
如： $C_1=P(x)\vee Q(a), C_2=\neg P(b)\vee R(x)$
解：
$\sigma = f(a)/x $; $x$ 用$f(a)$替换
$C_1\sigma = P(f(a))\vee Q(f(a))$,
选互补对：$L_1=P(f(a)),L_2=\neg P(y), \sigma = f(a)/y $
得归结式：$C_12=R(b)\vee Q(f(a))$