|
2.5.3 线性归结
线性归结是这样一种归结，首先从子句集S中选取一个称作顶子句的子句C0开始做归结，其次是归结过程中所得到的归结式Ci立即同另一子句Bi进行归结得归结式Ci+1。而Bi属于S或是已出现的归结式Cj(j<i)
 |
例: |
| S＝{P∨Q ,～P∨Q,P∨～Q,～P∨～Q} 选取顶子句C0＝P∨Q。 线性归结过程 (1) P∨Q (2) ～P∨Q (3) P∨～Q (4) ～P∨～Q (5) Q (1)(2) (6) P (5)(3) (7) ～Q (6)(4) (8) □ (7)(5) 顶子句的选择直接影响着归结的效率。如可选得C0使S－{C0}是可满足的。 |
2.5.4 单元归结和输入归结
在归结过程中，每次归结都有一个子句是单元（只含一个文字的）子句或单元因子时的归结称作单元归结。
一般地说，两子句归结式所含文字的个数，常常较这两个子句的每个所含文字个数都来得多。然而归结过程空子句的产生，必须来自两个只有单文字的子句如P和～P,于是归结式含文字的个数影响着归结的效率，单元归结具有明显的高效率，因为单元归结下的归结式所含文字个数，必是较长的那个被归结子句所含文字的个数减1。但是不难想像，单元归结不是完备的，如S是不可满足的，但不含单元子句时就不能使用单元归结。
|
例1: |
| S＝{P∨Q ,～P∨R,～Q∨ R,～R} 单元归结过程 (1) P∨Q (2) ～P∨R (3) ～Q∨R (4) ～R (5) ～P (4)(2) (6) ～Q (4)(3) (7) Q (5)(1) (8) P (6)(1) (9) R (7)(3) (10) □ (7)(6) |
单元归结与输入归结是一致的。即有从S到□的输入归结的充分必要条件是有从S到□的单元归结。它们都是不完备的归结方法。
|
例2: |
| S＝{P∨Q ,～P∨R,～Q∨ R,～R} 输入归结过程 (1) P∨Q (2) ～P∨R (3) ～Q∨R (4) ～R (5) Q∨R (1)(2) (6) R (3)(5) (7) □ (4)(6) |
例1及例2的子句集是相同的，分别采用了单元归结和输入归结的推理过程。