Key points are not available for this paper at this time.
Theoretical questions concerning the possibilities of proving theorems by machines are considered here from the viewpoint that emphasizes the underlying logic. A proof procedure for the predicate calculus is given that contains a few minor peculiar features. A fairly extensive discussion of the decision problem is given, including a partial solution of the (x)(Ey)(z) satisfiability case, an alternative procedure for the (x)(y)(Ez) case, and a rather detailed treatment of Skolem's case. In connection with the (x)(Ey)(z) case, an amusing combinatorial problem is suggested in Section 4.1. Some simple mathematical examples are considered in Section VI. Editor's Note. This is in form the second and concluding part of this paper' Part I having appeared in another journal. 1 However, an expansion of the author's original plan for Part II has made it a complete paper in its own right.
Hao Wang (Sun,) studied this question.