归结法基本原理
归结法的基本原理是采用反证法（也称反演推理法）将待证明的表达式（定理）转换成为逻辑公式（谓词公式），然后再进行归结，归结能够顺利完成，证明原公式（定理）是正确的。
def: Q 为 P_1,P_2, cdots ,P_n 的逻辑结论，当且仅当 Pwedge neg Q 是不可满足的，结论才成立
这样做的原因是证明不可满足性要比证明可满足性简单得多。通俗来讲，若要证明定理：张三是个好人。可以反向证明定理：张三不是个好人那是不可能的。
用符号公式表示就是:
置换转换为普通谓词公式:
再将其否定：
子句集
为了描述子句集，先给出如下几个名词的定义：
- 原子谓词公式：一个不能再分解的命题
- 文字：原子谓词公司及其否定 P: 正文字 neg P: 负文字
- 子句：任何文字的 析取式，任何文字本身也都是句子。
- 空子句：不包含任何文字的子句
- 子句集：所有子句的集合
例 1： 将下列谓词公式化为子句集
A. 利用一下公式消去谓词公式中的
Prightarrow QLeftrightarrow neg Pvee Q,Pleftrightarrow QLeftrightarrow (Pwedge Q)vee (neg Pwedge 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 (pwedge q)Leftrightarrow neg pvee neg q 量词否定转换率：neg exists xPLeftrightarrow forall xneg P,neg forall xPLeftrightarrow exists x neg P
color{red}{Longleftrightarrow} forall x(exists yneg 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 yneg 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 标准型的母式，即去掉所有量词的前束范式。 利用分配律： pvee(qwedge r)Leftrightarrow (pvee q)wedge (pvee r) pwedge(qvee r)Leftrightarrow (pwedge q)vee (pwedge 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 在不可满足的意义上是等价的（双向的）。
⭐️谓词逻辑中的归结原理：（含有变量的子句的归结）
谓词逻辑的归结比命题逻辑的归结要复杂得多，其中一个原因就是谓词逻辑公式中含有个体变量与函数。因此寻找互补的子句的过程就比较复杂。例如：
就不易从直接比较中发现这两个子句中含有的互补对，但如果将
置换与合一：（对个体变量做适当替换）
置换： 将子句中的变量做适当替换，可替换成常量、变量、Skolem 函数。 合一： 寻找相对变量的置换，使两个谓词公式一致
如： C_1=P(x)vee Q(a), C_2=neg P(b)vee R(x) 解： sigma = f(a)/x ; x 用 f(a) 替换 C_1sigma = 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))
