26
D.W. LOVELAND
information to be retained with each inference rule, information
such as when to give preference to the inference rule, as previ-
ously mentioned.
Overdirector or executive program -- a portion of the system
which is the top-level control. In the more sophisticated provers
the overdirector is more than a statistics keeper and link between
routines. An agenda is often maintained, which may be ·anything
from a scoring mechanism to resolve conflicting alternatives to an
active plan that develops the search along well prescribed lines.
There can be overdirectors at several levels in a hierarchy. A sam-
ple task of an overdirector is to terminate a branch of search
when the search effort is deemed "excessive" and backtrack lo
pursue a more promising path. The Bledsoe ATP prover [BTl] pro-
vides an excellent example of a significant overdirector.
Man-machine interaction -- the. close involvement of the user
in the proof search process. Although certain classes of problems
can be proven fully automatically quite quickly, the user can be
quite effective in cutting off "clearly" fruitless search paths or,
more positively, providing certain instantiations for key variables
that his experience suggests may be relevant or providing lemmas
the prover might attempt to prove and use. Most systems provide
for such interaction.
Advice -- direction from the builder or user that is superim-
posed upon the underlying proof scheme; The advice may be
encoded in a procedure, appear in the overdirector (e.g., in an
agenda design), or entered at runtime via man-machine interac-
tion. The latter use of advice is not restricted to human-oriented
provers.
Examples -- useful to help guide search, especially to suggest
instantiation of key variables. Examples help direct search down
possibly useful paths, which is an essential task faced in theorem
Previous Page Next Page