ALGEBRAIC TECHNIQUES AND THE MECHANIZATION OF NUMBER THEORY,
Abstract
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)
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 01, 1965
- Accession Number
- AD0612267
Entities
People
- Stephen A. Cook
Organizations
- RAND Corporation