proving formed the core of the reasoning component. The key to
using resolution for problem solving (as compared to theorem
proving) is answer extraction; such a procedure was given by
Green (see [Grl]).
The almost monolithic dedication to resolution during this
period brought sharp criticism from some AI researchers, notably
Marvin Minsky of MIT. By 1970, a Ph.D. student at MIT, Carl Hewitt,
had formulated a specific rebuttal to resolution, and to the logic
approach in general. He proposed PLANNER [Hel], a human-
oriented system not even a theorem prover per se, but a language
in which a "user" was to write his own theorem prover, specifically
tailored to the problem domain at hand. Besides this global com-
mitment to flexibility, the language itself was structured for flexi-
bility. For example, the inference rules could retain advice on
when the rule was to be activated, thus incorporating search con-
trol at the heart of the inference mechanism. Because each step
could be a procedure (a dynamic process) this approach has been
called a procedural approach to theorem proving. Although the
language was never fully implemented, a PLANNER subset was real-
ized (microPLANNER). We comment on use of procedures again
At the time that the opponents of resolution were making
themselves heard, a member of the resolution establishment,
Woody Bledsoe, was questioning the capability of uniform logic sys-
tems to handle the mathematics of set theory and analysis in par-
ticular. A proof of a simple problem involving the intersection of
families of sets proved awkward using resolution but fairly simple
using a backward chaining methodology with some quite basic set
theoretic inference rules. This observation began what is
definitely the most fruitful and sustained effort in human oriented
ATP to date. We return later to consider this approach to ATP.
Previous Page Next Page