Linear Resolution with Selection Function

Abstract

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 and/or search 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.