This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
August 1976 (vol. 25 no. 8)
pp. 782-801
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.
Index Terms:
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.
Citation:
G.A. Wilson, J. Minker, "Resolution, Refinements, and Search Strategies: A Comparative Study," IEEE Transactions on Computers, vol. 25, no. 8, pp. 782-801, Aug. 1976, doi:10.1109/TC.1976.1674697
Usage of this product signifies your acceptance of the Terms of Use.