{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,25]],"date-time":"2023-11-25T10:38:16Z","timestamp":1700908696353},"reference-count":9,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[1960,7]]},"abstract":"\n The hope that mathematical methods employed in the investigation of formal logic would lead to purely computational methods for obtaining mathematical theorems goes back to Leibniz and has been revived by Peano around the turn of the century and by Hilbert's school in the 1920's. Hilbert, noting that all of classical mathematics could be formalized within quantification theory, declared that the problem of finding an algorithm for determining whether or not a given formula of quantification theory is valid was the central problem of mathematical logic. And indeed, at one time it seemed as if investigations of this \u201cdecision\u201d problem were on the verge of success. However, it was shown by Church and by Turing that such an algorithm can not exist. This result led to considerable pessimism regarding the possibility of using modern digital computers in deciding significant mathematical questions. However, recently there has been a revival of interest in the whole question. Specifically, it has been realized that while no\n decision procedure<\/jats:italic>\n exists for quantification theory there are many proof procedures available\u2014that is, uniform procedures which will ultimately locate a proof for any formula of quantification theory which is valid but which will usually involve seeking \u201cforever\u201d in the case of a formula which is not valid\u2014and that some of these proof procedures could well turn out to be feasible for use with modern computing machinery.\n <\/jats:p>\n Hao Wang [9] and P. C. Gilmore [3] have each produced working programs which employ proof procedures in quantification theory. Gilmore's program employs a form of a basic theorem of mathematical logic due to Herbrand, and Wang's makes use of a formulation of quantification theory related to those studied by Gentzen. However, both programs encounter decisive difficulties with any but the simplest formulas of quantification theory, in connection with methods of doing propositional calculus. Wang's program, because of its use of Gentzen-like methods, involves exponentiation on the total number of truth-functional connectives, whereas Gilmore's program, using normal forms, involves exponentiation on the number of clauses present. Both methods are superior in many cases to truth table methods which involve exponentiation on the total number of variables present, and represent important initial contributions, but both run into difficulty with some fairly simple examples.<\/jats:p>\n \n In the present paper, a uniform proof procedure for quantification theory is given which is feasible for use with some rather complicated formulas and which does not ordinarily lead to exponentiation. The superiority of the present procedure over those previously available is indicated in part by the fact that a formula on which Gilmore's routine for the IBM 704 causes the machine to computer for 21 minutes without obtaining a result was worked successfully by\n hand computation<\/jats:italic>\n using the present method in 30 minutes. Cf. \u00a76, below.\n <\/jats:p>\n It should be mentioned that, before it can be hoped to employ proof procedures for quantification theory in obtaining proofs of theorems belonging to \u201cgenuine\u201d mathematics, finite axiomatizations, which are \u201cshort,\u201d must be obtained for various branches of mathematics. This last question will not be pursued further here; cf., however, Davis and Putnam [2], where one solution to this problem is given for ele<\/jats:p>","DOI":"10.1145\/321033.321034","type":"journal-article","created":{"date-parts":[[2002,7,27]],"date-time":"2002-07-27T11:25:57Z","timestamp":1027769157000},"page":"201-215","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1458,"title":["A Computing Procedure for Quantification Theory"],"prefix":"10.1145","volume":"7","author":[{"given":"Martin","family":"Davis","sequence":"first","affiliation":[]},{"given":"Hilary","family":"Putnam","sequence":"additional","affiliation":[]}],"member":"320","published-online":{"date-parts":[[1960,7]]},"reference":[{"key":"e_1_2_1_1_2","unstructured":"MARTIN DAVIS Computability and Unsolvability New York Toronto and London McGraw-Hill 1958 xxv + 210 pp. MARTIN DAVIS Computability and Unsolvability New York Toronto and London McGraw-Hill 1958 xxv + 210 pp."},{"key":"e_1_2_1_2_2","unstructured":"MANTIS DAvis AND HILARY PVTNAM A finitely axiomatizable system for elementary number theory. Submitted to Vhe Journal o} Symbolic Logic. MANTIS DAvis AND HILARY PVTNAM A finitely axiomatizable system for elementary number theory. Submitted to Vhe Journal o} Symbolic Logic."},{"key":"e_1_2_1_3_2","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1147\/rd.41.0028","article-title":"GILMOre, A proof method for quantification theory","volume":"4","author":"PAUL C","year":"1960","journal-title":"IBM J. Research Dev."},{"key":"e_1_2_1_4_2","unstructured":"JAcQues HERBRAND Recherches sur la thcorie de la demonstration. Travaux de la Societe des Sciences et des Lettres de Varsovie Classe III science mathematiques et physiques no. 33 128 pp. JAcQues HERBRAND Recherches sur la thcorie de la demonstration. Travaux de la Societe des Sciences et des Lettres de Varsovie Classe III science mathematiques et physiques no. 33 128 pp."},{"key":"e_1_2_1_5_2","unstructured":"DAVID HILBERT AND WILHELM ACKERM.4.NN Principles of Mathemabical Logic. New York Chelsea 1950 xii --k 172 pp. DAVID HILBERT AND WILHELM ACKERM.4.NN Principles of Mathemabical Logic. New York Chelsea 1950 xii --k 172 pp."},{"key":"e_1_2_1_6_2","volume-title":"Van Nostrand","author":"STEPHEN C.","year":"1952"},{"key":"e_1_2_1_7_2","unstructured":"WILLARD V. O. QUINE- Methods of Logic. New York Henry Holt revised 1959 xx W 272 PP. WILLARD V. O. QUINE- Methods of Logic. New York Henry Holt revised 1959 xx W 272 PP."},{"key":"e_1_2_1_8_2","doi-asserted-by":"crossref","first-page":"141","DOI":"10.2307\/2266900","article-title":"QUNIE, A proof procedure for quantification theory","volume":"20","author":"WILLARD V. O","year":"1955","journal-title":"J. Symbolic Logic"},{"key":"e_1_2_1_9_2","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1147\/rd.41.0002","article-title":"Towards mechanical mathematics","volume":"4","author":"HA WANG","year":"1960","journal-title":"IBM J. Research Dev."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/321033.321034","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T18:36:18Z","timestamp":1672511778000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/321033.321034"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1960,7]]},"references-count":9,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1960,7]]}},"alternative-id":["10.1145\/321033.321034"],"URL":"http:\/\/dx.doi.org\/10.1145\/321033.321034","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":["Artificial Intelligence","Hardware and Architecture","Information Systems","Control and Systems Engineering","Software"],"published":{"date-parts":[[1960,7]]},"assertion":[{"value":"1960-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}