Issue No.08 - August (1976 vol.25)
G.A. Wilson , Computer Science Laboratory, Naval Research Laboratory
This paper describes a comparative study of six binary inference systems and two search strategies employed in resolution-based problem solving systems. A total of 152 problems, most of which were taken from the recent literature, were employed. Each of these problems was attempted under a standard set of conditions using each inference system and each search strategy, for a total of twelve attempts for each problem. Using a variety of performance measures, a large number of hypotheses were examined in an effort to provide insight into the behavior of each inference system/search strategy combination. Whenever possible, the authors employed distribution-free statistical tests to minimize the subjectivity of the comparisons and hypothesis testing. Conclusions are presented concerning the effectiveness of the binary inference systems and search strategies, some effects of employing different problem representations, and certain characteristics of problems found to be significant in the overall system performance. Suggestions are made as to additional techniques that might enable theorem provers to solve practical problems.
Comparative analysis, linear resolution, P1 resolution, problem solving, proof procedure system, Q* algorithm, resolution inference, search strategies, set of support resolution, ?* algorithm, SL resolution, theorem proving.
G.A. Wilson, "Resolution, Refinements, and Search Strategies: A Comparative Study", IEEE Transactions on Computers, vol.25, no. 8, pp. 782-801, August 1976, doi:10.1109/TC.1976.1674697