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
Note: SRI Project 8776. The research reported herein was sponsored by National Science Foundation Grant GJ-1060.
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.
|Kling, Robert E||Alumnus|