第二章 归结推理方法

　　2.5.2 语义归结
　　一种语义归结策略是将子句S分成两部分，约定每部分内的子句间不允许做归结，还引入了文字次序，约定归结时其中的一个子句的被归结文字只能是该子句中"最大"的文字
例题 例:
  　S＝{～P∨～Q∨R,P∨R,Q∨R,～R}
　我们先规定S中出现的文字的次序，如依次为P，Q，R或记作P>Q>R。再选取S的一个解释I，如令
　　I＝{～P,～Q,～R}
　用它来将S分成两个部分。规定在I下为假的子句放入S1'中，在I下为真的子句放入S2'中。于是有
　　S1'={P∨R,Q∨R}
　　S2'＝{～P∨～Q∨R,～R}
　规定S1'内部的子句不允许归结，S1'与S2'子句间的归结必须是S 中的最大文字方可进行。这样所得的归结式，仍按I来放入S 或S2'。
　归结过程
　(1) ～P∨～Q∨ R ∈S2'
　(2) P∨R ∈S1'
　(3) Q∨R ∈S1'
　(4) ～R ∈S2'
　(5) ～Q∨R 　　 (2)(1)归结 ∈S2'
　(6) ～P∨R 　　 (3)(1)归结 ∈S2'
　(7) R 　　　　　(2)(6)归结 ∈S1'
　(8) R 　　　　　(3)(5)归结 ∈S1'
　(9) □ 　　　　 (7)(4)归结
　这是采用了语义归结策略下的盲目全面归结过程。明显地减少归结次数。阻止了(1)(4)的归结，也阻止了(2)(4)的归结。
　　另一语义归结称支持集策略。想法是简单，想要证明
　　　　　∧∧→B　　　成立
　　或　　∧∧∧～B　　不可满足
　　分析一下出现矛盾的原因，不会在，，间发生，自然是出于～B的引入，于是不必在找不到矛盾的，，间做归结了。
　　设S的子集T，说T是支持集，如果S－T是可满足的。
　　支持集归结策略，指的是从S到□的归结过程中，只选取不同时属于S－T的子句间进行归结。说得准确些每次做归结，至少有一个子句来自于T或由T导出的归结式。
例题 例:
  　S＝{P∨Q,～P∨R,～Q∨R，～R}
　取T＝{～R}
　支持集归结过程
　(1) P∨Q
　(2) ～P∨R
　(3) ～Q∨R
　(4) ～R
　(5) ～P 　　(2)(4)
　(6) ～Q 　　(3)(4)
　(7) Q 　　　(1)(5)
　(8) P 　　　(1)(6)
　(9) R 　　　(3)(7)
　(10) □ 　　(6)(7)
　这是采用了支持集策略的全面归结过程。
　所介绍的这两种语义归结都是完备的。