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 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

Abstract

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.

Electronic Copies


Adobe PDF

BibTeX

EndNote

AIC Personnel

Name Title E-mail
Kling, Robert E Alumnus
Raphael, Bertram Alumnus
Yates, Robert Alumnus

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