AUTOMATED THEOREM PROVING
3
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
Logic
approach ·and the
human-oriented
or
human simulation
approach. The
Logic
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
will
be exhibited as we pro-
gress; the thrust is obviously simulation of human problem solving
techniques.
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