The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.03 - Fall (1995 vol.17)
pp: 7-29
ABSTRACT
<p>This article reviews the history of the use of computers to automate mathematical proofs. It identifies three broad strands of work: automatic theorem proving where the aim is to simulate human processes of deduction; automatic theorem proving where any resemblance to how humans deduce is considered to be irrelevant; and interactive theorem proving, where the proof is directly guided by a human being. The first strand has been underpinned by commitment to the goal of artificial intelligence; practitioners of the second strand have been drawn mainly from mathematical logic; and the third strand has been rooted primarily in the verification of computer programs and hardware designs.</p>
CITATION
Donald MacKenzie, "The Automation of Proof: A Historical and Sociological Exploration", IEEE Annals of the History of Computing, vol.17, no. 3, pp. 7-29, Fall 1995, doi:10.1109/85.397057
REFERENCES
1. M. Davis, “The Prehistory and Early History of Automated Deduction,” in Automation of Reasoning: Classical Papers on Computational Logic, J. Siekmann and G. Wrightson, eds., Springer, Berlin, 1983, Vol. 1, pp. 1-28.
2. L. Wos and L. Henschen, “Automated Theorem Proving, 1965-1970,” in Automation of Reasoning: Classical Papers on Computational Logic, J. Siekmann and G. Wrightson, eds., Springer, Berlin, 1983, Vol. 2, pp. 1-24.
3. D.W. Loveland, “Automated Theorem Proving: A Quarter Century Review,” Contemporary Mathematics, Vol. 29, 1984, pp. 1-45.
4. D.J. O’Leary, “Principia Mathematicaand the Development of Automated Theorem Proving,” in Perspectives on the History of Mathematical Logic, T. Drucker, ed., Boston, Birkhäuser, 1991, pp. 48-53.
5. G. Lolli, La Macchina e le Dimostrazioni: Matematica, Logica e Informatica, il Mulino, Bologna, 1987.
6. T.L. Heath, The Thirteen Books of Euclid’s Elements, Cambridge Univ. Press, Cambridge, 1908.
7. Heath, Euclid’s Elements, pp. 155.
8. G. Leibniz, “Elements of a Calculus,” in Leibniz: Logical Papers—A Selection, G.H.R. Parkinson, ed., Clarendon Press, Oxford, 1966, pp. 17-24, quotation on pp. 18.
9. G. Frege, Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Nebert, Halle, 1879.
10. A.N. Whitehead and B. Russell, Principia Mathematica (second edition), Cambridge Univ. Press, Cambridge, 1925, Vol. 1, pp. 94-95 and 132.
11. K. Gödel, “über Vollständigkeit und Widerspruchsfreiheit,” Ergebnisse eines mathematischen Kolloquiums, Vol. 3, 1931, pp. 12-13.
12. K. Gödel, “über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme I,” Monatshefte für Mathematik und Physik, Vol. 38, 1931, pp. 173-198.
13. Lolli, La Macchina e le Dimostrazioni, pp. 13-25.
14. H. Mehrtens, Symbolische Imperative: Zu Natur und Beherrschungsprogramm des wissenschaftlichen Moderne. In , Die Modernisierung moderner Gesellschaften: Verhandlungen des 25. Deutschen Soziologentages in Frankfurt am Main 1990, Campus, Frankfurt am Main, 1991, pp. 604-616.
15. H. Poincaré, Science et Méthode,Flammarion, Paris, 1908, pp. 157 (my translation).
16. H. Mehrtens, Moderne Sprache Mathematik: Eine Geschichte des Streits um die Grundlagen der Disziplin und des Subjekts formaler Systeme, Suhrkamp, Frankfurt am Main, 1990.
17. A.M. Turing, “On Computable Numbers, with an Application to theEntscheidungsproblem,” Proc. London Mathematical Soc., Series 2, Vol. 42, 1939, pp. 230-265.
18. N. Bourbaki, Elements of Mathematics: Theory of Sets, Addison Wesley, Reading, Mass., 1968, pp 11.
19. R.S. Boyer and J.S. Moore, “A Theorem Prover for a Computational Logic,” keynote address to 10th Conf. on Automated Deduction, 1990, pp. 8.
20. P.H. Nidditch, Introductory Formal Logic of Mathematics, Univ. Tutorial Press, London, 1957, pp. v, 1, and 6-7.
21. W.S. Jevons, “On the Mechanical Performance of Logical Inference,” Philosophical Trans. of the Royal Soc., Vol. 160, 1870, pp. 497-518.
22. P. McCorduck, Machines Who Think.San Francisco: W.H. Freeman, 1979.
23. H.A. Simon, Models of My Life.New York: Basic Books, 1991. Reissued by MIT Press, 1996.
24. H. Simon interviewed by A. Dale, Pittsburgh, Apr.21, 1994.
25. McCorduck, Machines Who Think, pp. 116.
26. A. Newell, J.C. Shaw, and H. Simon, “Empirical Explorations of the Logic Theory Machine: A Case Study in Heuristic,” Proc. Western Joint Computer Conf., Vol. 15, 1957, pp. 218-239, quotations on pp. 219.
27. Newell, Shaw, and Simon, “Empirical Explorations of the Logic Theory Machine,” pp. 221.
28. O’Leary, “Principia Mathematicaand the Development of Automated Theorem Proving,” pp. 52.
29. B. Russell, letter to Herbert Simon, Nov. 2, 1956, quoted in O’Leary , “Principia Mathematica and the Development of Automated Theorem Proving,” pp. 52.
30. P. McCorduck, Machines Who Think.San Francisco: W.H. Freeman, 1979.
31. Newell, Shaw, and Simon, “Empirical Explorations of the Logic Theory Machine,” pp. 220.
32. Simon interviewed by Dale.
33. D. Crevier, AI: The Tumultuous History of the Search for Artificial Intelligence, Basic Books, New York, 1993, pp. 52-54.
34. H.L. Gelernter and N. Rochester, “Intelligent Behavior in Problem-Solving Machines,” IBM J. Research and Development, Vol. 2, 1958, pp. 336-345.
35. H. Gelernter, J.R. Hansen, and D.W. Loveland, “Empirical Explorations of the Geometry-Theorem Proving Machine,” in Computers and Thought, E.A. Feigenbaum and J. Feldman, eds., McGraw-Hill, New York, 1963, pp. 153-163, quotation on pp. 153.
36. Simon interviewed by Dale.
37. H. Wang, “Toward Mechanical Mathematics,” IBM J. Research and Development, Vol. 4, 1960, pp. 2-21, quotation on pp. 3.
38. Wang, “Toward Mechanical Mathematics,” pp. 18.
39. K. Gödel, “Die Vollständigkeit der Axiome des logischen Funktionenkalküls,” Monatshefte für Mathematik und Physik, Vol. 37, 1930, pp. 349-360.
40. B. Dreben, “On the Completeness of Quantification Theory,” Proc. National Academy of Sciences, Vol. 38, 1952, pp. 1047-1052.
41. W.V. Quine, “A Proof Procedure for Quantification Theory,” J. Symbolic Logic, Vol. 20, No. 2, June 1955, pp. 141-149.
42. D. Prawitz, “Preface to‘A Mechanical Proof Procedure . . .’,” in Automation of Reasoning: Classical Papers on Computational Logic, J. Siekmann and G. Wrightson, eds.,Springer, Berlin, 1983, Vol. 1, pp. 200-201.
43. M. Presburger, “über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt,” in Sprawozdanie z I Kongresu matematyków krajów slowianskich, Warszawa 1929, Sklad Glówny, Warsaw, 1930, pp. 92-101.
44. M. Davis interviewed by A.J. Dale, New York, Apr.29, 1994.
45. M. Davis, “A Computer Program for Presburger’s Algorithm,” paper presented to Cornell Summer Institute for Symbolic Logic, 1957, in Automation of Reasoning: Classical Papers on Computational Logic, J. Siekmann and G. Wrightson, eds., Springer, Berlin, 1983, Vol. 1, pp. 41-48.
46. Wang, “Toward Mechanical Mathematics.”
47. H. Wang, “Proving Theorems by Pattern Recognition,” Comm. ACM, Vol. 4, No. 3, 1960, pp. 229-243.
48. Wang, “Toward Mechanical Mathematics,” pp. 4.
49. E.W. Beth, “On Machines which Prove Theorems,” Simon Stevin Wis- en Natur-kundig Tijdschrift, Vol. 32, 1958, pp. 49-60, quotation on pp. 59.
50. A. Robinson, “Proving a Theorem (as Done by Man, Logician, or Machine),” in Automation of Reasoning: Classical Papers on Computational Logic, J. Siekmann and G. Wrightson, eds.,Springer, Berlin, 1983, Vol. 1, pp. 74-76, quotation on pp. 74.
51. P.C. Gilmore, “A Proof Method for Quantification Theory: Its Justification and Realization,” IBM J. Research and Development, Vol. 4, 1960, pp. 28-35.
52. Wang, “Toward Mechanical Mathematics.”
53. D. Prawitz, H. Prawitz, and N. Voghera, “A Mechanical Proof Procedure and its Realization in an Electronic Computer,” J. ACM, Vol. 7, 1960, pp. 102-128.
54. Gilmore, “Proof Method for Quantification Theory.”
55. J.A. Robinson interviewed by A.J. Dale, Edinburgh, Feb.15 and 16, 1994.
56. W.F. Miller letter to author, June18, 1993.
57. M. Davis and H. Putnam, "A Computing Procedure for Quantification Theory," J. ACM, vol. 7, July 1960, pp. 201-215.
58. D. Prawitz, “An Improved Proof Procedure,” Theoria, Vol. 26, 1960, pp. 102-139.
59. J.A. Robinson,“A machine-oriented logic based on the resolution principle,” J. of the ACM, vol. 12, no. 1, pp. 23-41, Jan. 1965.
60. Robinson ,interviewed by Dale.
61. For a recent survey, see J.A. Robinson, "Logic and Logic Programming," Comm. ACM, vol. 35, no. 3, Mar. 1992, pp. 40-65.
62. J. Fleck, “Development and Establishment in Artificial Intelligence,” in Scientific Establishments and Hierarchies: Sociology of the Sciences Yearbook, Vol. VI, N. Elias, H. Martins, and R. Whitley, eds., Reidel, Dordrecht, 1982, pp. 169-217.
63. D.W. Loveland, Automated Theorem Proving: A Logical Basis,North-Holland, Amsterdam, 1978.
64. Robinson, “Logic and Logic Programming,” p. 45.
65. Crevier, AI, p. 64.
66. S. Papert interviewed by A.J. Dale, Cambridge, Mass., June7, 1994.
67. M. Minsky, S. Papert, and staff, Proposal to ARPA for Research on Artificial Intelligence at M. I. T., 1971-1972, MIT Artificial Intelligence Memo No. 245, 1971, pp. 13-14.
68. P.J. Hayes, “A Critique of Pure Treason,” Computational Intelligence, Vol. 3, 1987, pp. 179-185, quotations on pp. 183.
69. R.A. Kowalski, “The Early Years of Logic Programming,” Comm. ACM, Vol. 31, No. 1, 1988, pp. 38-42.
70. Sir J. Lighthill, “Artificial Intelligence: A General Survey,” in Artificial Intelligence: A Paper Symposium, Science Research Council, London, 1973, p. 10.
71. S. A. Cook,“The Complexity of Theorem-Proving Procedures,”Proc. 3rd Ann. ACM Symposium on Theory of Computing,New York: Association for Computing Machinery, 1971, pp. 151–155.
72. C. Cherniak, “Computational Complexity and the Universal Acceptance of Logic,” J. Philosophy, Vol. 81, No. 12, Dec. 1984, pp. 739-758.
73. W.W. Bledsoe, “I Had a Dream: AAAI Presidential Address, 19 Aug. 1985,” AI Magazine, Vol. 7, 1986, pp. 57-61, quotation on pp. 57.
74. A.O. Boyer and R.S. Boyer, “A Biographical Sketch of W.W. Bledsoe,” in Automated Reasoning: Essays in Honor of Woody Bledsoe, R.S. Boyer, ed., Kluwer, Dordrecht, 1991, pp. 1-29.
75. W.W. Bledsoe, “Non-Resolution Theorem Proving,” Artificial Intelligence, Vol. 9, 1977, pp. 1-35, quotation on pp. 2-3.
76. C. Hewitt, Description and Theoretical Analysis (using Schemas) of Planner: A Language for Proving Theorems and Manipulating Models in a Robot, PhD thesis, MIT, Cambridge, 1971.
77. Bledsoe, “Non-Resolution Theorem Proving,” p. 12.
78. Loveland, “Automated Theorem Proving,” p. 24.
79. W.W. Bledsoe, “Splitting and Reduction Heuristics in Automatic Theorem Proving,” Artificial Intelligence, Vol. 2, 1971, pp. 55-77, quotations on pp. 55.
80. A.P. Morse, A Theory of Sets, Academic Press, New York, 1965.
81. Bledsoe, “Splitting and Reduction Heuristics,” p. 66.
82. W.W. Bledsoe, R.S. Boyer, and W.H. Henneman, “Computer Proofs of Limit Theorems,” Artificial Intelligence, Vol. 3, 1972, pp. 27-60, quotations on pp. 28 and 35, and details of the procedure on pp. 35-38.
83. L.T. Wos et al., “The Concept of Demodulation in Theorem Proving,” J. ACM, Vol. 14, No. 4, Oct. 1967, pp. 698-709.
84. G. Robinson and L. Wos, “Paramodulation and Theorem-Proving in First-Order Theories with Equality,” Machine Intelligence, Vol. 4, 1969, pp. 135-150.
85. S. Winker and L. Wos, “Automated Generation of Models and Counterexamples and its Application to Open Questions in Ternary Boolean Algebra,” Proc. Eighth Int’l Symp. Multiple-valued Logic, Rosemont, Ill., IEEE and ACM, New York, 1978, pp. 251-256.
86. S. Winker, L. Wos, and E.L. Lusk, “Semigroups, Antiautomorphism, and Involutions: A Computer Solution to an Open Problem, I,” Mathematics of Computation, Vol. 37, 1981, pp. 533-545.
87. S. Winker, “Generation and Verification of Finite Models and Counterexamples Using an Automated Theorem Prover Answering Two Open Questions,” J. ACM, Vol. 29, No. 2, 1982, pp. 273-284.
88. L. Wos, “Solving Open Questions with an Automated Theorem-Proving Program,” in Proc. Sixth Conf. Automated Deduction,New York , June 7-9, 1982, D.W. Loveland, ed., Springer, New York , 1982, pp. 1-31.
89. L. Wos et al., “Questions Concerning Possible Shortest Single Axioms for the Equivalential Calculus: An Application of Automated Theorem Proving to Infinite Domains,” Notre Dame J. Formal Logic, Vol. 24, No. 2, 1983, pp. 205-223.
90. T.S. Kuhn, The Structure of Scientific Revolutions, 2nd ed., Univ. of Chicago Press, Chicago, 1970.
91. L. Wos, “Transition to the Future,” J. Automated Reasoning, Vol. 9, No. 1, 1992, pp. iii.
92. J.R. Guard et al., “Semi-Automated Mathematics,” J. ACM, Vol. 16, 1969, pp. 49-62, quotation on pp. 49.
93. R. Bumcrot, “On Lattice Complements,” Proc. Glasgow Mathematical Assn., Vol. 7, 1965, pp. 22-23.
94. Guard et al., “Semi-Automated Mathematics,” p. 58.
95. N.G. de Bruijn, “Automath: A Language for Mathematics,” in Automation of Reasoning: Classical Papers on Computational Logic, J. Siekmann and G. Wrightson, eds., Springer, Berlin, 1983, Vol. 2, pp. 159-200, quotation on pp. 159.
96. E.G.H. Landau, Grundlagen der Analysis, Akademische Verlag, Leipzig, 1930.
97. L.S. van Benthem Jutting, Checking Landau’s“Grundlagen”in the Automath System, PhD thesis, Technische Hogeschool, Eindhoven, 1977.
98. P.J. Davis and R. Hersh, “Rhetoric and Mathematics,” in The Rhetoric of the Human Sciences, J.S. Nelson et al., eds., London , Univ. of Wisconsin Press, 1987, pp. 53-68, quotation on pp. 63-64.
99. P. Naur and B. Randell, eds., Software Engineering: Report of a Conference Sponsored by the NATO Science Committee, Garmisch, Germany, 7-11 Oct. 1968, NATO, Brussels, 1969.
100. E. Peláez, A Gift from Pandora’s Box: The Software Crisis, PhD thesis, Univ. Edinburgh, 1988.
101. H.H. Goldstine and J. von Neumann, “Planning and Coding of Problems for an Electronic Computing Instrument,” in John von Neumann: Collected Works, Vol. V,A.H. Taub, ed., Pergamon, Oxford, 1963, pp. 80-151.
102. A.M. Turing, “Checking a Large Routine,” in Report of a Conference on High Speed Automatic Calculating Machines, Cambridge Univ. Mathematical Laboratory, Cambridge, 1949, pp. 67-69, reprinted in F.L. Morris and C.B. Jones,“An Early Program Proof by Alan Turing,”Annals of the History of Computing, Vol. 6, No. 2, Apr. 1984, pp. 139-143.
103. C.B. Jones, The Search for Tractable Ways to Reason about Programs, Univ. Manchester, Dept. of Computer Science, UMCS-92-4-4, 1992, p. 8.
104. J. McCarthy, “Towards a Mathematical Science of Computation,” in Information Processing 1962: Proc. IFIP Congress 62, C.M. Popplewell, ed., North Holland, Amsterdam, 1963, pp. 21-28.
105. P. Naur, “Proof of Algorithms by General Snapshots,” BIT, Vol. 6, 1966, pp. 310-316.
106. R.W. Floyd, “Assigning Meanings to Programs,” Mathematical Aspects of Computer Science: Proc. Symposia in Applied Mathematics, Vol. 19, 1967, pp. 19-32.
107. C.A.R. Hoare, "An Axiomatic Basis for Computer Programming," Comm. ACM, 1969.
108. J. McCarthy and J. Painter, “Correctness of a Compiler for Arithmetic Expressions,” in Mathematical Aspects of Computer Science: Proc. Symposia in Applied Mathematics, Vol. 19, 1967, pp. 33-41.
109. R.L. London, “Computer Programs Can Be Proved Correct,” in Theoretical Approaches to Non-Numerical Problem Solving: Proc. Fourth Systems Symp. at Case Western Reserve Univ., Springer, Berlin, 1970, pp. 281-302.
110. J.C. King, A Program Verifier, PhD thesis, Carnegie Mellon Univ., 1969, p. 166.
111. King, Program Verifier.
112. D.I. Good, Toward a Man-Machine System for Proving Program Correctness, PhD thesis, Univ. of Wisconsin, 1970.
113. D.I. Good personal communication.
114. D.E. Bell and L.J. LaPadula, Secure Computer Systems: Mathematical Foundations, Mitre Corp., Bedford, Mass. , MTR-2547, 1973.
115. D.I. Good, “Mechanical Proofs about Computer Programs,” Philosophical Trans. of the Royal Soc. of London, Series A, Vol. 312, 1984, pp. 389-409, quotation on pp. 389.
116. W.W. Bledsoe and P. Bruell, “A Man-Machine Theorem-Proving System,” in Advance Papers of Third Int’l Joint Conf. Artificial Intelligence, W.W. Bledsoe, ed., Vol. 5, Part 1, 1974, pp. 51-72.
117. D.I. Good, “Proof of a Distributed System in Gypsy,” in Formal Specification: Proc. Joint IBM/Univ. of Newcastle upon Tyne Seminar, 7-10 Sept., 1983, M.J. Elphick, ed., Univ. of Newcastle upon Tyne, Computing Laboratory, 1983, pp. 44-89, quotation on pp. 61.
118. D.I. Good, interviewed by E. Peláez, Austin, Tex., May 16, 1991.
119. Good, “Proof of a Distributed System in Gypsy.”
120. M. Schaefer, “Symbol Security Condition Considered Harmful,” Proc. 1989 IEEE Symp. Security and Safety, IEEE CS Press, Los Alamitos, Calif., 1989, pp. 20-46, especially pp. 26.
121. Department of Defense, Trusted Computer System Evaluation Criteria, National Computer Security Center, Fort Meade, Md. , DOD 5200.28-STD, 1985.
122. For descriptions of them, see M.H. Cheheyl, M. Gasser, G.A. Huff, and J.K. Millen, "Verifying Security," Computing Surveys, vol. 13, pp. 279-339, Sept. 1981.
123. C.L. Gold, S.E. Goodman, and B.G. Walker, “Software: Recommendations for an Export Control Policy,” Comm. ACM, Vol. 23, No. 4, 1980, pp. 199-207, quotations on pp. 199 and 203.
124. G. Pottinger, Proof Requirements in the Orange Book: Origins, Implementation, and Implications , typescript, Feb. 11, 1994.
125. Boyer and Moore, “Theorem Prover for a Computational Logic,” p. 1.
126. R.S. Boyer interviewed by A.J. Dale, Austin, Tex., Apr. 8, 1994.
127. J.S. Moore interviewed by A.J. Dale, Austin, Tex., Apr. 7, 1994.
128. R.S. Boyer and J.S. Moore, A Computational Logic, Academic Press, New York, 1979, pp. xiii.
129. R. Burstall, “Proving Properties of Programs by Structural Induction,” Computer J., Vol. 12, 1969, pp. 41-48.
130. R.S. Boyer and J.S. Moore, “Proving Theorems about LISP Functions,” J. ACM, Vol. 22, No. 1, 1975, pp. 129-144.
131. Boyer and Moore, A Computational Logic, pp. xiv.
132. Boyer interviewed by Dale.
133. Boyer and Moore, “Theorem Prover for a Computational Logic,” p. 4.
134. Boyer interviewed by Peláez.
135. R. Pollack interviewed by A.J. Dale, Edinburgh, Nov. 15, 1993.
136. Boyer and Moore, “Theorem Prover for a Computational Logic,” p. 3.
137. R. Boyer and J. Moore, A Computational Logic Handbook. New York: Academic Press, 1988.
138. N. Shankar, Proof-checking Metamathematics, PhD thesis, Univ. of Texas at Austin, 1986.
139. R. Milner interviewed by A.J. Dale, Edinburgh, Nov. 17 and 30, 1993.
140. R. Milner, Logic for Computable Functions: Description of a Machine Implementation, Stanford Univ., Stanford Artificial Intelligence Project, AIM-169, 1972.
141. M. Gordon, R. Milner, and C. Wadsworth, Edinburgh LCF, Univ. of Edinburgh, Dept. of Computer Science, CSR-11-77, 1977.
142. Stuart Anderson, personal communication.
143. R. Milner, LCF: A Way of Doing Proofs with a Machine, Univ. of Edinburgh, Dept. of Computer Science, CSR-41-79, 1979, p. 3.
144. Gordon, Milner, and Wadsworth, Edinburgh LCF, p. 5.
145. L.C. Paulson, Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge Univ. Press, Cambridge, 1987, p. 209.
146. W.P. van Stigt, Brouwer’s Intuitionism,North-Holland, Amsterdam, 1990.
147. R.L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System.Englewood Cliffs, N.J.: Prentice Hall, 1986.
148. F.K. Hanna and N. Daeche, “Specification and Verification Using Higher-Order Logic: A Case Study,” in Formal Aspects of VLSI Design, G.J. Milne and P.A. Subrahmanyam, eds., North-Holland, Amsterdam, pp. 179-213, quotation on pp. 180.
149. P.B. Andrews et al., “Automating Higher-Order Logic,” Contemporary Mathematics, Vol. 29, 1984, pp. 169-192.
150. M. Gordon, “HOL: A Machine Oriented Formulation of Higher-Order Logic,” Univ. of Cambridge, Computer Laboratory, Tech. Report 103, 1985.
151. A. Cohn, “A Proof of Correctness of the Viper Microprocessor: The First Level,” Univ. of Cambridge, Computer Laboratory, Tech. Report No. 104, 1987.
152. M. Gordon interviewed by D. MacKenzie, Cambridge , Jan. 10, 1991.
153. Loveland, “Automated Theorem Proving.”
154. W.W. Bledsoe, “A New Method for Proving Certain Presburger Formulas,” Advance Papers of Fourth Int’l Joint Conf. Artificial Intelligence, Tbilisi, 3-8 Sept. 1975, pp. 15-21.
155. D. Loveland interviewed by D. MacKenzie, Edinburgh , Aug. 25, 1993.
156. Loveland, “Automated Theorem Proving.”
157. A.J. Nevins, “A Human Oriented Logic for Automatic Theorem-Proving,” J. ACM, Vol. 21, No. 4, 1974, pp. 606-621.
158. Robinson, “Machine-Oriented Logic Based on the Resolution Principle.”
159. L. Wos, “Automated Reasoning Answers Open Questions,” Notices of the American Mathematical Soc., Vol. 40, No. 1, 1993, pp. 15-26, quotation on pp. 16.
160. D.B. Lenat, AM: An Artificial Intelligence Approach to Discovery in Mathematics as Heuristic Search, PhD thesis, Stanford Univ., 1976.
161. H. Wang, “Computer Theorem Proving and Artificial Intelligence,” Contemporary Mathematics, Vol. 29, 1984, pp. 49-70, quotation on pp. 49-50.
162. Simon interviewed by Dale.
163. Wang, “Toward Mechanical Mathematics,” p. 3.
164. J.A. Robinson, “Formal and Informal Proofs,” in Automated Reasoning: Essays in Honor of Woody Bledsoe, R.S. Boyer, ed., Kluwer, Dordrecht, 1991, pp. 267-282.
165. Wang, “Computer Theorem Proving and Artificial Intelligence,” p. 60.
166. H.A. Simon and A. Newell, “Heuristic Problem Solving: The Next Advance in Operations Research,” Operations Research, 6, 1958, pp. 1-10, quotation on pp. 7.
167. E.A. Feigenbaum and J. Feldman,eds., Computers and Thought, McGraw-Hill, New York, 1963.
168. Anon., “The Talk of the Town,” The New Yorker, June 11, 1966, pp. 27-28.
169. H.L. Dreyfus, What Computers Can’t Do: The Limits of Artificial Intelligence, Harper&Row, New York, 1979, p. 293.
170. Wang, “Toward Mechanical Mathematics,” p. 3.
171. Dreyfus, What Computers Can’t Do, p. 300.
172. Wang, “Computer Theorem Proving and Artificial Intelligence,” p. 65.
173. Lighthill, “Artificial Intelligence,” pp. 10 and pp. 20.
174. Robinson, “Formal and Informal Proofs,” p. 269.
175. D. Hilbert, “The Foundations of Mathematics,” in From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931,J. van Heijenoort, ed., Harvard Univ. Press, Cambridge, Mass., 1967, pp. 464-479, quotation on pp. 465.
176. D. Gorenstein, “The Enormous Theorem,” Scientific American, Vol. 253, No. 6, Dec. 1985, pp. 92-103, quotation on pp. 92.
177. R. DeMillo, interviewed by A.J. Dale, Chicago, Sept. 1994.
178. R. Lipton, interviewed by A.J. Dale, Princeton, N.J.,
179. Richard A. DeMillo, Richard J. Lipton, and Alan J. Perlis, "Social Processes and Proofs of Theorems and Programs," Comm. ACM, vol. 22, p. 271, May 1979.
180. K. Appel and W. Haken, “Every Planar Map is Four Colorable,” Illinois J. Mathematics, Vol. 21, 1977, pp. 429-567.
181. F.F. Bonsall, “A Down-to-Earth View of Mathematics,” American Mathematical Monthly, Vol. 89, 1982, pp. 8-14, quotations on pp. 13-14.
182. D.I.A. Cohen, “The Superfluous Paradigm,” in The Mathematical Revolution Inspired by Computing, J.H. Johnson and M.J. Loomes, eds., Clarendon, Oxford, 1991, pp. 323-329, quotation on pp. 328.
183. D.I.A. Cohen, interviewed by A.J. Dale, New York, May2, 1994.
184. M. Schaefer, interviewed by Garrel Pottinger, Rockville, Md., Mar.23, 1993.
185. D. MacKenzie, “The Fangs of the VIPER,” Nature, Vol. 352, No. 6335, Aug.8, 1991, pp. 467-468.
5 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool