14 D.W. LOVELAND

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

later.

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.