
AUTOMATED THEOREM PROVING 16
the consequences of certain statements using forward chaining.
This is usually triggered directly by the statement itself. For
example, if a premise employs,.symbols not in a common "vocabu
lary", it is often wise to seek consequences that employ the more
common symbols. This increases the chance of a match with a
subgoal to close off a branch of the search tree. In general, the
combinatorics of node explosion with depth of search suggests bi
directional search.
If
twenty steps separate goal from premises, it
is more efficient search to expand ten steps from each than
twenty steps from the goal in all directions. Of course, one usually
knows less about which premise to expand than which goal, so one
biases the search in favor of the goal. However, Nevins in [Ne2]
makes a case for a strong forward chaining bias.
Types to utilize different domains of objects over which vari
ables range. If one distinguishes variables that range over
integers from variables that range over reals (or variables over
individuals from variables over sets) one realizes considerable
efficiency in processing because restriction to the chosen domain
is builtin rather than treated axiomatically, which requires
deduction. By having the type builtin, the pattern matching (e.g.,
unification) on terms is considerably more powerful.
Procedures  a mechanism of integrating search control with
inference. Decision procedures are one extreme where a sentence
is fully evaluated to true or false under control of the algorithm
being used. At the other extreme are procedural heuristics that
alter search ftow in a minor way.
As
a simple example of pro
cedural heuristics, statements that are frequently established in
one step might be expanded first and established immediately if
successful, so as to quickly reduce the number of unproven goals.
This was done in the geometry theorem prover [GHl]. Hewitt's
theorem proving language PLANNER [Hel] allows for procedural