DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
ALGEBRAIC TECHNIQUES AND THE MECHANIZATION OF NUMBER THEORY,
RAND CORP SANTA MONICA CALIF
Pagination or Media Count:
A number of mechanical procedures for generating proofs of theorems of logic have appeared in the literature, all based on the Skolem-Herbrand theorem. Although in principle the procedures can be applied to find proofs of mathematical theorems, the procedures are very inefficient for this purpose because they are designed to operate on too large a domain. This report outlines a general method by which these procedures can be adapted to operate more efficiently on a much more restricted domain the statements of elementary number theory. The method is given a theoretical justification, and several specific algorithms are described for realizing the general method. These algorithms are applied to examples. Much more detailed study must be done before the method can be successfully utilized by a computer to generate proofs of difficult number-theoretic theorems. Author
APPROVED FOR PUBLIC RELEASE