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
Previous Page Next Page