Skip to main content

Proving Theorems by Pattern Recognition - II

01 January 1961

New Image

TECHNICAL VOLUME XL Copyright 1961, American Telephone and JOURNAL NUMBER Telegraph Company 1 JANUARY 1961 Proving Theorems by Pattern Recognition -- II By HAO WANG (Manuscript received J u l y 18, 1960) 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 J^.l. Some simple mathematical examples are considered in Section VI. Editor's ATote. This is in form the second and concluding part of this paper' P a r t 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.