第二章 归结推理方法

　　2.5 归结过程的控制策略

　　尽管归结推理方法比直接使用Herbrand 定理做推理是有了明显的进步，然而使用归结法时，若从子句集S出发做所有可能的归结，并将归结式加入S中，再做第二层这样的归结，…直到产生空子句的这种盲目的全面归结的话，同样会产生组合爆炸问题。这种无控制的盲目全面归结会导致大量的不必要的归结式的产生，严重的是它们又将产生下一层的更大量的不必要的归结式的产生。于是，如何给出控制策略，以使仅只对选择合适的子句间方可做归结来避免多余不必要的归结式的出现，或说少做些归结但仍然导出空子句来，这已成为极重要的问题了。
　　举例来说明盲目归结带来的困难。
例题 例:
  　S＝{P∨Q,～P∨Q，P∨～Q,～P∨～Q} 来证明是不满足的。
　证明过程是从S0＝S 出发。依次构造
　Si={,的归结式│∈S0∪S1…∪Si-1,∈Si-1} i=1,2,…,直至出现空子句□证明结束。这就是盲目全面归结的描述。具体的归结过程是
　S0 (1)P∨ Q 　　　　　　(2) ～P∨Q
　　 (3)P ∨～Q 　　　　　(4)～P∨～Q
　S1 (5)Q 　(1)(2) 　　　 (6)P　 　　　　 (1)(3)
　　 (7)Q∨～Q (1)(4) 　　(8)P∨～P 　　　(1)(4)
　　 (9)Q ∨～Q (2)(3) 　 (10) P∨～P 　　(2)(3)
　　 (11)～P (2)(4) 　　　(12)～Q 　　　　(3)(4)
　S2 (13)P ∨Q (1)(7) 　　(14) P∨ Q 　　 (1)(8)
　　 (15)P∨ Q (1)(9) 　　(16)P∨ Q 　　　(1)(10)
　　 (17)Q (1)(11) 　　　 (18)P 　　　　　(1)(12)
　　 (19)Q (2)(6) 　　　　(20)～P∨ Q 　　(2)(7)
　　 (21) ～P ∨Q (2)(8)　(22)～P∨ Q 　　(2)(9)
　　 (23)～P ∨Q (2)(10)　(24)～P 　　　　(2)(12)
　　 (25)P (3)(5)　　　　 (26)P∨～Q 　　 (3)(7)
　　 (27)P ∨～Q (3)(8) 　(28)P ∨～Q 　　(3)(9)
　　 (29)P∨～Q　(3)(10)　(30)～Q 　　　　(3)(11)
　　 (31)～P (4)(5)　　　 (32)～Q 　　　　(4)(6)
　　 (33)～P∨～Q (4)(7)　(34)～P ∨～Q 　(4)(8)
　　 (35)～P∨ ～Q (4)(9) (36)～P∨ ～Q 　(4)(10)
　　 (37) Q (5)(7)　　　　(38)Q 　　　　　(5)(9)
　　 (39) □ (5)(12)
在这种归结过程中产生了相当数量的不必要的归结式。一类是重言式如(7)－(10)，由它们又产生了归结式(13)�D(16)，(20)－(23)，(26)�D(29)，(33)－(39)。另一类是重复的，如P,Q,～P,～Q就多次出现过。
　就这个例子而言，若由人来证明只需三步，(5)(12)(39)便得空子句，这节将介绍删除策略、语义归结和线性归结等控制策略。
　　2.5.1 删除策略
　　设有两个子句C和D，若有置换σ使得
　　　　CσD 成立，便说子句C把子句D归类。
例题 例:
  　C＝P(X)　　D＝P(a)∨Q(a) 取σ＝{a/x},便有
　Cσ= P(a){P(a),Q(a)}而{P(a),Q(a)}的逻辑表示就是D＝P(a)∨Q(a)。于是C把D归类。
　　若对S使用归结推理过程中，当归结式Cj是重言式或Cj被S中子句或归结式Ci(i<j)所归类时，便将Cj删除。这样的推理过程便称作使用了删除策略的归结过程。
　　判别归结式是否重言式是简单的，因归结式也是子句是文字的析取，只需检查归结式中有无互补对便可实现。然而判别C是否把D归类就不这么简单了，但有算法。
　　删除策略对阻止不必要的归结式的产生来缩短归结过程是有效的。然而要在归结式Cj产生后方能判别它是否可被删除，这部分计算量是要花费的，只是节省了被删除的子句又生成的归结式。尽管使用删除策略的归结，少做了归结但不影响产生空子句，就是说使用删除策略的归结推理是完备的。
　　现在讨论归类算法。
　　给了子句C，D。令
　　　θ＝{a1/,…,an/}
其中,…,是出现于D中的所有变量。a1,…,an是C，D中未出现的常量。
　　设　D ＝L1∨…∨Lm
　　　　Dθ＝L1θ∨…∨Lmθ　是基子句了。
　　　　～Dθ＝～L1θ∧…∧～Lmθ
　　归类问题本是Cσ与D中部分文字合一的问题，作了上述准备，便化成了Cσ与～Dθ的归结问题了。由于依归类的定义，不允许D的变量做置换的，所以先将D中元素以常量代入，为用归结法自然要将Dθ取否定。
　　归类算法
　　(1) 令W＝{～L1θ,…,～Lmθ}
　　(2) 令K＝0，U0＝{C}
　　(3) 如果Uk包含□，停止，这时C把D归类。否则令UR+1＝{,的归结式│∈Uk,∈W}　　　
　　(4) 如果Uk+1是空集，停止，这时C不能把D归类。否则K+1→K转(3)
例题 例:
  　C ＝～P(x) ∨(Q(f(x),a)
　D =～P(h(y))∨(Q(f(h(y)),a)∨P(z)
　使用归类算法可知C 把D归类
　先作θ＝{b/y,c/z}
　　　Dθ=～P(h(b)) ∨Q(f(h(b)),a)∨ P(c)
　　　～Dθ={P(h(b)),～Q(f(h(b)),a),～P(c)}
　(1)W={ P(h(b)),～Q(f(h(b)),a),～P(c)}
　(2)U0={C}={～P(x) ∨Q(f(x),a)}
　(3)U0不包含□，作
　　 U1={Q(f(h(b)),a),～P(h(b))}
　(4)U1不空□
　(5)U2含□
　从而C把D归类。