LINEAR RESOLUTION WITH SELECTION FUNCTION
LINEAR RESOLUTION WITH SELECTION FUNCTION
复制标题
DOI：
10.1016/0004-3702(71)90012-9
复制
发表时间：
1971-01-01
影响因子：
14.4
通讯作者：
KUEHNER, D
中科院分区：
文献类型：
--
作者：
KOWALSKI, R;KUEHNER, D
带选择函数的线性归结（SL-归结）是线性归结的一种限制形式。主要的限制是由一个选择功能，从每个子句选择一个单一的文字，在该子句中解决。这个和其他限制是适应线性分辨率从洛夫兰的模型elimination.We表明，SL-分辨率实现了大量减少冗余和不相关的衍生物的产生，这样做，而不会显着增加最简单的证明的复杂性。SL-分解的一个更深远的优点是它适合于启发式搜索。特别地，分类树、子目标、引理和/或搜索树都可以用来提高查找反驳的效率。这些考虑表明SL-归结的优越性，定理证明程序构造的启发式吸引力，从与其他定理证明方法的比较，我们推测，最好的证明程序的一阶逻辑将通过进一步阐述SL-归结。
Linear resolution with selection function (SL-resolution) is a restricted form of linear resolution. The main restriction is effected by a selection function which chooses from each clause a single literal to be resolved upon in that clause. This and other restrictions are adapted to linear resolution from Loveland's model elimination.We show that SL-resolution achieves a substantial reduction in the generation of redundant and irrelevant derivations and does so without significantly increasing the complexity of simplest proofs. We base our argument for the increased efficiency of SL-resolution upon precise calculation of these quantities.A more far reaching advantage of SL-resolution is its suitability for heuristic search. In particular, classification trees, subgoals, lemmas, and/orssearch trees can all be used to increase the efficiency of finding refutations. These considerations alone suggest the superiority of SL-resolution to theorem-proving procedures constructed solely for their heuristic attraction.From comparison with other theorem-proving methods, we conjecture that best proof procedures for first order logic will be obtained by further elaboration of SL-resolution.