第二章 归结推理方法

　　2.4.2 归结式
　　在谓词逻辑下求两个子句的归结式，和命题逻辑一样消互补对，但需考虑变量的合一与置换。
　　设、 是两个无公共变量的子句，L1、L2分别是、的文字，如果 L1与～L2 有mgu σ，则
　　　　　(σ-{L1σ})∪(σ -{L2σ})
称作子句、 的一个二元归结式，而L1、L2为被归结的文字。
　　这里使用了集合的符号和运算，是为了说明的方便。要将子句Ciσ、Liσ先写成集合形式，如P(x)∨～Q(y)改写为{P(x),～Q(y)}。在集合的表示下作减法和作并集运算，然后再写成子句形，如集合运算结果为{P(x),～Q(y)}改写为P(x)∨～Q(y)。
　　归结式定义中，要求、 无公共变量也是合理的。如=P(x)=～P(f(x)),而
　　　　　S＝{、 }
　　是不可满足的，但、 的变量是相同的，就无法合一了，从而没有归结式了。也即不能用归结法证明S的不可满足性了，这就限制了归结法的使用范围，如果对C1或C2的变量使用易名规则，便可将C1、C2化成无共同的变量了。这是没问题的，如S＝{P(x)∨Q(y),R(y)∨Q(y)}其逻辑表示是
　　S＝(x)(y)((P(x) ∨～Q(y)) ∧ (R(y)∨Q(y)))
　　 = (x)(y)((P(x) ∨～Q(y)) ∧(x)(y)(R(y)∨Q(y)))
　　 = (x)(y)((P(x) ∨～Q(y)) ∧(y)(R(y)∨Q(y)))
　　 = (x)(y)((P(x) ∨～Q(y)) ∧(z)(R(z)∨Q(z)))
　　写成集合形式
　　　　　S＝{P(x)∨～Q(y),R(z)∨Q(z)}
　　同命题逻辑下归结式的定义不同的是，先需对、 有关变量作mgu,再消去互补对。
　　同样有
　　　　　∧R(,)
　　其中R(,)表示, 的二元归结式。
例题 例1:
  　 =～A(x)∨B(x)
　 = A(a)∨D(y)
　R(,) = B(a)∨D(y)
例题 例2:
  　 =～A(x)∨B(x)
　 = A(g(x))
　先将的变量改写为y，便可对　
　　　 ＝～A(y)∨B(y)
　　　 ＝A(g(x))
　作归结了，R(,)＝B(g(x)))。实际计算过程中不必写出换变量这一步，而只需将, 的变量想作是不同的就可以了。
例题 例3:
  　 =P(x)∨Q(x)
　 =～P(g(y))∨～Q(b)∨R(x)
这样的,有两个二元归结式，取σ1={g(y)/x}得
　　　R(,) =Q(g(y))∨～Q(b)∨R(x)
　而取σ2={b/x}，便有R(,) =P(b)∨～P(g(y))∨R(x)
例题 例4:
  　 =P(x)∨～Q(b)
　 =～P(a)∨Q(y)∨R(z)
　这时注意，求归结式不能同时消去两个互补对。如在σ＝{a/x,b/y}下　得 R(z)。这不是, 的二元归结式。最简单的例子是
　　　 =P∨Q, =～P∨～Q
　若消两个互补对便得空子句□。但是, 并无矛盾。或说消两个互补对的结果并不是, 的逻辑推论了。所以消两个互补对的结果不是二元归结式。

　　在对子句作归结前，可先考虑子句内部的化简，这便提出了子句因子概念。
　　设　C= P(x)∨P(f(x))∨～Q(x)
　　令　σ={f(y)/x}
　　置换σ使用于C，可使P(x),P(f(y))合一，Cσ较C来得简单了。
　　如果一个子句C的几个文字有mguσ，那么C的例Cσ称作子句C的因子。
定义 定义
  　若, 是无公共变量的子句，作
　(1) ,的二元归结式
　(2) 的因子和的二元归结式
　(3) 和的因子的二元归结式
　(4) 的因子和的因子的二元归结式
　这四种二元归结式都叫子句, 的归结式，仍记作R(,)。
例题 例5:
  　 =P(x)∨P(f(y))∨Q(g(y))
　 =～P(f(g(a)))∨Q(b)
　先作C1的因子，取σ={f(y)/x} 得C1的因子
　　　　　　　　　σ =P(f(y))∨Q(g(y))
　于是有, 的归结式
　　　R(,)=Q(g(g(a)))∨Q(b)
　, 到R(,) 的推理仍是正确的。