全句推导

Whole-clause Resolution

摘要: 在一般的单元归结（unit-resolution）中,证明一个子句S是不可满足的,通常是从S中取一个子句C,然后设法将C中的文字逐次归结掉,最后得出空子句.在归结某文字时,一般是在子句集中盲目搜索可与该文字归结的单元子句;可能在归结到某一步时,发现由该子质推导不出空子句,再取另一个子句重新归结.另外,对于一个子句C=L₁,L₂…L_n,由于选择文字进行归结的次序不同,可能有很多重复性的工作.

Abstract: Here we propose the concept of whole-clause resolution which is better than unit-resolution.From a non-unit clause we can deduce the empty-clause or unit clauses by using the whole-clause resolution without producing many unrelated middle clauses,thus eliminating redundant work for trial.