4
D.W. LOVELAND
we give a very limited treatment of that energetic period ( 1965-
1970) and refer the interested reader to Chang and Lee [CLl] or
Loveland (Lo5] for {detailed) information on resolution theorem
proving. We do not mean to imply that resolution is unimportant
{quite the contrary, as we hope to convey) but allows us to con-
centrate more on the period 1970-1982. For those interested in
the original papers of this field, through the early 1970's, see the
Siekmann and Wrightson anthology [SWl].
Throughout this review we give a year associated with many of
the contributions for relative perspective. As an exact year is
sometimes hard to determine for an ongoing project or because of
publication delay after the result has been announced informally,
dates must be regarded as approximate.
Figure 1 lists a number of major contributions, listed accord-
ing to their bias towards the logic or human simulation approach.
The Presburger prover programmed by Martin Davis {1954),
already mentioned, was a straight implementation of the classical
Presburger decision procedure for additive number theory;
roughly, first order sentences about linear equalities and inequali-
ties over the domain of non-negative integers. A decision pro-
cedure for a theory is a precise recipe (procedure, algorithm) that
halts for any well-formed sentence in the domain and outputs
"true" (or "valid") if that indeed is the case. The complexity of the
decision procedure is high (as is now better understood) so the
program proved only very simple facts.
The Logic Theorist (LT) previously mentioned is the ack-
nowledged first published exploration in automated theorem prov-
ing. Its goal was to mechanically simulate the deduction processes
of humans as they prove propositional logic theorems. The
methods used were, first, substitution into established formulae to
directly obtain a desired result, or, failing that, to find a
Previous Page Next Page