采用支撑集策略时,从开始到得到e的整个归结过程中,只选取不同时属于S-T的子句,在其间进行归结。就是说,至少有一个子句来自于支撑集T或由T导出的归结式。
例如:A1∧A2∧A3∧~B中的~B可以作为支撑集使用。要求每一次参加归结的亲本子句中,只要应该有一个是有目标公式的否定(~B)所得到的子句或者它们的后裔。
支撑集策略的归结是完备的,同样,所有可归结的谓词公式都可以用采用支撑集策略达到加快归结速度的目的。问题是如何寻找合适的支撑集。一个最容易找到的支撑集是目标子句的非,即S~B。 |