J. A. Robinson

A REVIEW

OF AUTOMATIC THEOREM-PROVING

1. Introduction. The basic formalism. By a theorem-proving problem we

mean a problem which has the form: show that B follows from A1, • • •, An,

where A1 ..., An and B are statements. It may well be that A1, •••,An

are the axioms or postulates of some theory, and that B is a (presumed)

theorem of that theory; in that case the problem is that of proving the

given theorem from the given axioms.

It is usually thought that such problems require a certain amount of

ingenuity for their solution, and indeed it is by using mathematical skill

and ingenuity in reasoning that people usually solve them. However, under

very general conditions on the language in which the statements A1, • • •, An

and B are expressed (so general that, as far as one can tell, any statement

ever uttered, or ever likely to be uttered, in a mathematical context, can

be expressed suitably in a language which meets them), a theorem-proving

problem can be solved automatically if it can be solved at all. That is to

say, if the given B does follow from the given Au -—,An then this fact

can be detected, automatically, by executing a certain purely clerical

algorithm on Ax, — -,An and B as input. As a by-product of the ensuing

computation there will be constructed a proof (in a suitable sense) of B

from Au • • •, An.

These very general conditions are those that characterize the so-called

first-order predicate calculus. In order that this paper may be read more

or less independently, this formalism will now be briefly described, in a

quantifier-free version which avoids several complications which are not

really germane to our present purposes. The relationship between this

version of the first-order predicate calculus and versions which contain

quantifiers is well discussed in Davis and Putnam [2] and in Davis [3].

A single nonempty collection D of entities, the so-called universe of dis-

course, is supposed to be understood; symbols, called relation symbols, are

available to denote relations over D, i.e., functions from

Dn,

the set of all

n-tuples of elements of D, (where n is the degree of the relation and of the

l