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

Design Implications of Theorem-Proving Strategies

by Kling, Robert E.

Technical Note 44
Institution: AI Center, SRI International
Address: 333 Ravenswood Ave, Menlo Park, CA 94025
Oct 1970.

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

Order an AIC Technical Note

Abstract

QA3.6 is a new resolution theorem prover that allows a user to flexibly elect subsets of pre-set strategies and to easily state strategies of is own. Presumably, some strategies will in fact be expressionable within hours after conception, while others may require days or weeks and require modifying the system. Currently, when a user wishes to add new strategy to the old QA3.5 he must modify certain system functions. Frequently several functions must be modified and the flow of information rerouted nontrivially. Furthermore, a QA3.5 user must be intimately familiar with the various internal representations and system structure in order to write a successful strategy. We hope to design QA3.6 so that a strategy writer need not know much, if anything about the internal representations and information flows. He will be able to work in a language which is closer to the vernacular of resolution logic, e.g., clauses, literals, resolvents, etc, than to the language of implementation, e.g., caar, cadar, etc. In order to facilitate this goal, it is likely that the best design of QA3.6 would create a series of check past which all information of certain kinds would flow. Thus, to add a particular (selection or delection) strategy would require modifying only one well understood section of QA3.6 rather than several clever, but idiosyncratically-chosen spots. Presumably, such well-defined changes could be automated for most users.

Electronic Copies


Adobe PDF

BibTeX

EndNote

AIC Personnel

Name Title E-mail
Kling, Robert E Alumnus

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