ABSTRACT
Obviously we have not listed all the blind alleys and the method has to be specified much more exactly before a machine program can be written. But, it is thought, the above outline makes it plausible that a fairly natural program can be written on existing machines to prove theorems like i and, for example, also 2x2 ^ y 2 (x, y range over positive integers).
