删除策略的相容性

ON COMPATIBILITY OF DELETION STRATEGY

本文给出关于删除策略相容性的几个结果：对相同谓词符号配相同锁的子句集，锁归结和删除策略联用完备；对正文字锁大于负文字锁的Horn集，正单元锁归结和删除策略联用完备，输入锁归结与删除策略联用完备；配锁Horn集上输入半锁归结和删除策略联用完备；标准Horn集上正单元强有序归结和删除策略联用完备，强有序输入归结和删除策略联用完备．

Some results on compatibility of deletion strategy are obtained in thispaper. Using deletion strategy, lock resolution is complete for the clause set whereliterals with the same predicate symbol have the same index: both positive unit lockresolution and input lock resolution are complete for the Horn set where the indexesof positive literals are greater than the indexes of negative literals;input half-lockresolution is complete for Horn set; both positive unit strong ordered resolution andstrong ordered input resolution are complete for standard Horn set.