1961/01/01 by Hao Wang · 875 citations
Computer Science · Mathematics · #Calculus (dental) #Combinatorics #Computability, Logic, AI Algorithms #Computer science #Connection (principal bundle) #Discrete mathematics #Epistemology #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Philosophy #Predicate (mathematical logic) #Programming language #Satisfiability #Section (typography) #Simple (philosophy)
paper · doi:10.1002/j.1538-7305.1961.tb03975.x
published in Bell System Technical Journal 40(1), 1-41 (Institute of Electrical and Electronics Engineers)
openalex publication_date 1961/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/31
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.1However, an expansion of the author's original plan for Part II has made it a complete paper in its own right.