Search |  Contact |  SRI Home Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap.A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A ASRI International.  333 Ravenswood Avenue.  Menlo Park, CA 94025-3493. SRI International is a nonprofit corporation.

Publication in EndNote Format

%0 Report %@ 75 %A Reboh, Rene, Raphael, Bertram, Yates, Robert A., Kling, Robert E., and Velarde, Carlos %T Study of Automatic Theorem-Proving Programs %C 333 Ravenswood Ave, Menlo Park, CA 94025 %I AI Center, SRI International %D 1972 %K Theorem-Proving, QA3.6 %X 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. %O SRI Project 8776. The research reported herein was sponsored by the National Science Foundation under Grant GJ-1060. %U http://www.ai.sri.com/pubs/files/1506.pdf

SRI International
©2014 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy