×

Automation of reasoning. 1: Classical papers on computational logic 1957–1966. (English) Zbl 0567.03001

Symbolic Computation. Artificial Intelligence. Berlin etc.: Springer- Verlag. XII, 525 p. DM 98.00 (1983).
The beginnings of computer mechanized theorem proving are located in the middle of the fifties. Step by step the results accumulated, the importance of the field grew continually. The last decade marked an extraordinary development, revealing the fundamental importance of automated reasoning in computer modelling of cognitive processes.
The idea to select and publish the most influential papers on computational logic is one of the most valuable and inspired editorial acts. The selection of the papers, made by the editors in close cooperation with an international advisory committee, was a very difficult task, taking almost three years of careful evaluation of those ideas, papers and authors proved to be fruitful and becoming classics. The result was gathered in two volumes, covering respectively the periods 1957-1966 and 1967-1970. Unavoidable omissions were necessary to keep the two volumes within manageable size. However, additional volumes are planned in the same series, to cover the non-included fields (theorem proving in higher order calculi, non-classical logic, applications of theorem proving in program synthesis, question answering, problem solving, program verification, robot technology, programming languages), and the work in computational logic which appeared after 1970.
The first two papers in the volume are survey papers: M. Davis: ”The prehistory and early history of automated deduction” (pp. 1-28), a review of the idea evolution about the automation of reasoning in mathematics, from Déscartes and Leibniz to the last decades, marked by the computer influence; S. Yu. Maslov, G. E. Mints and V. P. Orevkov: ”Mechanical proof-search and the theory of logical deduction in the USSR” (pp. 29-38).
The following papers are listed according to the year of appearance, being followed by authors’ commentaries on errors, history and current evaluation. Since further commentaries are needless in this case, we consider most useful just to list the selected papers. Also needless to say how useful the complete bibliography of 450 titles at the end of each volume is, covering (and including) the period up to 1970.
M. Davis: ”A computer program for Presburger’s algorithm” (pp. 41- 48) [Summaries Summer Inst. Symb. Logic, Cornell Univ. 1957, 215-223 (1960; Zbl 0171.271)]; A. Newell, J. C. Shaw and H. A. Simon: ”Empirical explorations with the logic theory machine: A case study in heuristics” (pp. 49-73) [Proc. West. Joint Comp. Conf., 218-239 (1957)]; A. Robinson: ”Proving a theorem (as done by man, logician or machine)” (pp. 74-76) [Summaries of Talks Presented at the Summer Inst. for Symb. Logic. Commun. Res. Div., Inst. for Defense Analysis, Princeton, New Jersey (1957)]; E. W. Beth: ”On machines which prove theorems” (pp. 79-90) [Simon Stevin 32, 49-60 (1958; Zbl 0084.250)]; B. Dunham, R. Fridshal and G. L. Sward: ”A non-heuristic program for proving elementary logical theorems” (pp. 93-98) [Information Processing, Proc. Int. Conf. Information Processing, UNESCO, Paris, June 15-20, 1959, 282-285 (1960; Zbl 0115.352)]; H. Gelernter: ”Realization of a geometry-theorem proving machine” (pp. 99-122) [ibid. 273-282 (1960; Zbl 0114.069)]; M. Davis and H. Putnam: ”A computing procedure for quantification theory” (pp. 125-139) [J. Assoc. Comput. Mach. 7, 201-215 (1960; Zbl 0212.342)]; H. Gelernter, J. A. Hansen and D. W. Loveland: ”Empirical explorations of the geometry-theorem proving machine” (pp. 140-150) [Proc. West. Joint. Comp. Conf., May 1960, 143-147 (1960); reproduced in Computers and Thought, 153-167 (New York, 1963)]; P. C. Gilmore: ”A proof method for quantification theory: Its justification and realization” (pp. 151-161) [IBM J. Res. Develop. 4, 28-35 (1960; Zbl 0097.003)]; D. Prawitz: ”An improved proof procedure” (pp. 162-201) [Theoria 26, 102-139 (1960; Zbl 0099.008)]; D. Prawitz, H. Prawitz and N. Voghera: ”A mechanical proof procedure and its realization in an electronic computer” (pp. 202-228) [J. Assoc. Comput. Mach. 7, 102-128 (1960; Zbl 0213.024)]; H. Wang: ”Proving theorems by pattern recognition. I” (pp. 229-243) [Commun. ACM 3, 220-234 (1960; Zbl 0101.105)]; H. Wang: ”Toward mechanical mathematics” (pp. 244-264) [IBM J. Res. Develop. 4, 2-27 (1960; Zbl 0097.004)]; M. Davis, G. Logemann and D. Loveland: ”A machine program for theorem proving” (pp. 267-270) [Commun. ACM 5, 394-397 (1962; Zbl 0217.540)]; B. Dunham and J. H. North: ”Theorem testing by computer” (pp. 271-275) [Proc. Symp. Math. Theor. Automata, New York, April 24-26, 1962, 173-177 (1963; Zbl 0116.346)]; B. Dunham, R. Fridshal and J. H. North: ”Exploratory mathematics by machine” (pp. 276-287) [Information and Decision Processes (New York, 1962)]; H. Gelernter: ”Machine- generated problem-solving graphs” (pp. 288-312) [Proc. Symp. Math. Theor. Automata, New York, April 24-26, 1962, 179-203 (1963; Zbl 0158.162)]; M. Davis: ”Eliminating the irrelevant from mechanical proofs” (pp. 315-330) [Proc. Symp. Appl. Math. 15, 15-30 (1963; Zbl 0131.012)]; J. Friedman: ”A semi-decision procedure for the functional calculus” (pp. 331-354) [J. Assoc. Comput. Mach. 10, 1-24 (1963; Zbl 0144.244)]; J. Friedman: ”A computer program for a solvable case of the decision problem” (pp. 355-363) [ibid. 10, 348-356 (1963; Zbl 0118.332)]; S. Kanger: ”A simplified proof method for elementary logic” (pp. 364-371) [Comput. Programm. Formal Systems, 87-94 (1963; Zbl 0217.009)]; J. A. Robinson: ”Theorem-proving on the computer” (pp. 372- 383) [J. Assoc. Comput. Mach. 10, 163-174 (1963; Zbl 0109.356)]; L. T. Wos, D. F. Carson and G. A. Robinson: ”The unit preference strategy in theorem proving” (pp. 387-393) [AFIPS Proc. Fall Joint Comput. Conf., San Francisco, October 1964, 26 Part 1, 615-621 (1964; Zbl 0135.183)]; J. A. Robinson: ”A machine oriented logic based on the resolution principle” (pp. 397-415) [J. Assoc. Comput. Mach. 12, 23-41 (1965; Zbl 0139.123)]; J. A. Robinson: ”Automatic deduction with hyper-resolution” (pp. 416-423) [Int. J. Comput. Math. 1, 227-234 (1965; Zbl 0158.260)]; N. A. Shanin, G. V. Davydov, S. Yu. Maslov, G. E. Mints, V. P. Orevkov and A. O. Slisenko: ”An algorithm for a machine search of a natural logical deduction in a propositional calculus” (pp. 424-483) [translation of the Russian original (Moskva-Leningrad, 1965; Zbl 0168.014)]; L. T. Wos, G. A. Robinson and D. F. Carson: ”Efficiency and completeness of the set of support strategy in theorem proving” (pp. 484- 489) [J. Assoc. Comput. Mach. 12, 536-541 (1965; Zbl 0135.184)]; B. Meltzer: ”Theorem-proving for computers: Some results on resolution and renaming” (pp. 493-495) [Computer J. 8, 341-343 (1966; Zbl 0158.260)]; Bibliography on computational logic (pp. 497-525).
Reviewer: N.Curteanu

MSC:

03-06 Proceedings, conferences, collections, etc. pertaining to mathematical logic and foundations
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
01A75 Collected or selected works; reprintings or translations of classics