|
| |
6.归结策略
(1)归结的一般过程
设有子句集S={C1,C2,C3,C4}其中C1,C2,C3,C4是S中的子句，计算机对此子句集进行归结的一般过程是：
①从子句C1开始，逐个与C2,C3,C4进行比较，看那两个子句可进行归结。然后用C2与C3进行比较，归结。最后用C3和C4比较，归结。得到第一级归结式。
②再从C1开始，用S中的子句分别与第一级归结式中的子句逐个地进行比较，归结，得第二级归结式。
③仍然从C1开始，用S中的子句集第一级归结式中的子句逐个地与第二级归结式中的子句进行比较，得第三级归结式。
继续直到出现空子句或者不能再继续归结为止。只要子句集是不可满足的，上述归结过程一定会归结出空子集而终止。
|
  点击看详解 |
 点击看详解 |
| |
|
|
