ABSTRACT
The eventual goal of studying new uses of computers must be practical in a broad sense. They may be used to do familiar things in order to eliminate drudgery, to reduce cost, to increase reliability, or to speed up operations. The initial experiment with and limited success at automatic demonstration came from an appreciation of the fairly advanced state which mathematical logic had arrived at with respect to formalization. Mathematical activity is a phenomenon in nature and is, as such, like all mechanical and mental activities, finite. Familiar connections between mathematical logic and automatic computers are the possibility of representing basic building blocks of computers by Boolean functions and the close resemblance between programming languages and symbolisms of logic. One might think of the examples familiar from high school mathematics: clever word problems in arithmetic become a matter of routine in algebra, and ingenious proofs in elementary geometry can be treated systematically in analytic geometry.
