and the Intermediate Value (IV) theorem (Bledsoe [B12], also this
volume) have been proven by automated provers. (The IV theorem
had the least upper bound principle as given.)
One of the most interesting ways to view the progression of
this field is by identifying the two major approaches, or philo-
sophic viewpoints adopted, and reviewing contributions in this
light. We call the two approaches the
approach ·and the
human simulation
approach. The
approach is characterized by the presence of a dominant logical
system that is carefully delineated and essentially static over the
development stage of the theorem proving system. Also, search
control is clearly separable from the logic and can be regarded as
sitting "over" the logic. Control "heuristics" exist but are syntax-
directed primarily. We shall include modular decision procedures
augmenting systems as quite within the spirit of the logic
approach. The
human simulation
approach generally is the
antithesis of the above. Specific traits
be exhibited as we pro-
gress; the thrust is obviously simulation of human problem solving
The logic and human simulation approaches are admittedly
not clearly delineated nor will ATP systems generally fit neatly in
one extreme or the other. We make no further apology for this.
The distinct philosophies represented in the two approaches have
been very important historically and thus it is instructive to con-
sider the influence of each approach even on systems not strictly.
in one camp.
A reader wishing a fuller review of the early history of ATP
than space permits us may consult Davis' paper "The prehistory
and early history of automated deduction" (see Davis [Da2]). The
Davis paper covers to the mid-1960's. The late 1960's saw an
intense investigation of the resolution principle of J.A. Robinson;
Previous Page Next Page