Publication Details

Study of Automatic Theorem-Proving Programs

by Reboh, Rene, Raphael, Bertram, Yates, Robert A., Kling, Robert E., and Velarde, Carlos

Technical Note 75
Institution: AI Center, SRI International
Address: 333 Ravenswood Ave, Menlo Park, CA 94025
Nov 1972.

Note: SRI Project 8776. The research reported herein was sponsored by the National Science Foundation under Grant GJ-1060.

Order an AIC Technical Note

A first-order, resolution based theorem-proving program (QA3.6), specially designed to allow experimentation with resolution strategies, was implemented and used to compare the performances of various combinations of refinements of simple resolutions. We present statistics and comment on the use of various strategies. The following strategies and refinements were studied: set-of-support, ancestry-filter, merging, model strategies, unit preference, end-test for quick proof, subsumption, and length, depth, and level bounds. The experimental results demonstrate the usefulness of the end-test for quick proof, and the power of well-chosen model strategies. Merging and ancestry-filter strategies proved to be somewhat disappointing.