知识表示与推理

谓词逻辑的归结推理

合一

• 可理解为：通过给公式里的变量找合适的替换，来让几个公式变得一模一样
• 设公式集$F=\{F_1,F_2,\dots ,F_n\}$，如果存在一个置换 $\lambda$，使得$F_1\lambda =F_2\lambda =\cdots =F_n\lambda$，那么这个 $\lambda$ 就叫做这个公式集的一个合一，而$F_1,\dots ,F_n$就叫做可合一的。

例子：

• 设有公式集$F=P(x,y,f(y)),P(a,g(x),z)$，则$\lambda =a/x,g(a)/y,f(g(a))/z$
• 这里注意每个位置的值要跟着已有参数来，是$g(a)$而不是$g(x)$

最一般合一（MGU Most General Unifier）

• 差异集：即从左往右找出第一个同位置不同的项构成的集合（当前两个式子中，最先出现的那一对不同子项）
• 步骤：
  1. 先初始化，原公式集相同，初始置换取恒等置换
  2. 检查两式子是否相同
  3. 从左到右，从外到内，找第一处不同的子项
  4. 若其中一个是变量，另一个是项，并且这个变量不出现在那个项中，就可以做代换。${\theta }_0=\{a/z\}$（变量代换为常量）
  5. 两个都是常量且不同，例如 $\{a,b\}$，那就不能合一，算法结束。
  6. 两个都是复合项，但最外层函数符号不同，例如 $\{f(x),g(x)\}$，也不能合一。
  7. 变量出现在它要代换成的项里面，例如想令 $x\mapsto f(x)$，这不允许，叫出现检查失败，也不能合一。
  8. 用刚找到的代换作用到当前公式集上，得到新公式集
  9. 若二者还不同，重复上述过程

归纳语言

设子句写成： $(L_1,L_2,L_3,\dots )$ 那么一般有：

• a 表示第1个文字
• b 表示第2个文字
• c 表示第3个文字
• d 表示第4个文字

所以：

• 1a = 第1个子句第1个文字
• 1b = 第1个子句第2个文字
• 2a = 第2个子句第1个文字
• 2c = 第2个子句第3个文字

对于： $R[1a,2c][X=a](Q(g(a)),R(a),Q(z))$

就是：

将第1个子句中的第1个文字 P(x) 和第2个子句中的第3个文字 $\neg P(a)$作为冲突文字， 用最一般合一 $\{x=a\}$ 做归结， 得到新子句 $(Q(g(a)),R(a),Q(z))$。

可判定与不可判定

• 可判定问题：如果存在一个算法或过程，该算法用于求解该类问题时，可在有限步内停止，并给出正确的解答。
• 不可判定问题：不存在上述的算法或过程则称这类问题是不可判定的

归结过程

等价于证明 $KB\cup \{\neg HardWorker(sue)\}$ 是不可满足的，也就是能归结出空子句 NIL。 所以先把结论取反，加进知识库。

子句集：

(1)$(\neg GradStudent(x),Student(x))$

(2)$(\neg Student(x),HardWorker(x))$

(3)$(GradStudent(sue))$

(4)$(\neg HardWorker(sue))$

归结过程：

(5)$[1,3]\{sue/x\}(Student(sue))$

(6)$[2,5]\{sue/x\}(HardWorker(sue))$

(7)$[4,6]NIL$

• $\forall xP(x)\vee \forall yQ(y)\Rightarrow 1.P(x)\vee Q(y)$
• $\neg \forall x(P(x)\vee Q(x))\iff \exists x(\neg P(x)\wedge \neg Q(x))\Rightarrow 2.\neg P(a)及3.\neg Q(a)$
• $R[1,2]\{x=a\}\Rightarrow 4.Q(y)$
• $R[3,4]\{y=a\}()$

• $1.R(x)\vee L(x)$
• $2.\neg D(y)\vee \neg L(y)$
• $3.I(f)$
• $4.D(f)$
• $5.\neg I(z)\vee R(z)$
• $R[2,4]\{y=f\}\Rightarrow 6.\neg L(f)$
• $R[1,6]\{x=f\}\Rightarrow 7.\neg R(f)$
• $R[5,7]\{z=f\}\Rightarrow 8.\neg I(f)$
• $R[3,8]()\Rightarrow 9.NIL(空子句)$

归结策略

• 宽度有先策略
• 删除策略（纯文字删除法、重言式删除法、包孕删除法）
• 支持集策略
• 线性输入策略
• 单文字策略
• 祖先过滤策略

一般步骤

• 要证$KB|=f$，等价于证明$KB\wedge \neg f$
• 子句在转换时要全部变为析取集合
• 将结论取反再变为析取式放入子句集
• 如果原来是合取，那就变成两个子句
• 在子句集中用逗号表示$\vee$
• 实质上使用析取三段式来不断推出子句
• 直到推出空子句为止

1. $(\neg R(x),L(x))//将第一个式转为析取$
2. $(\neg D(y),\neg L(y))//将第二个式转为析取$
3. $I(a)//第三个式合取的一项$
4. $D(a)//第三个式合取的另一项$
5. $(\neg I(z),R(z))//结论取反变为析取式后存在量词变全部$
6. $R[3,5a]\{z=a\}R(a)//R表示resolution，方括号中表示其由哪两个子句归结得到$
7. $R[1a,6]\{x=a\}L(a)$
8. $R[2b,7]\{y=a\}\neg D(a)$
9. $R[4,8]()$