Principia Mathematica and the Development of Automated Theorem Proving
The present chapter describes the first two major published works in automated theorem proving, the Logic Theory Machine (LT) of Newell, Shaw, and Simon about 1956 and the work of Wang in 1958. Both works attempted to prove theorems in propositional logic found in Principia Mathematica. While the LT is the first published example of automated theorem proving, Martin Davis, in 1954, wrote a program to prove theorems in additive arithmetic (Loveland, 1984, p. 1). His results were not published.
KeywordsExecutive Director Propositional Logic Theorem Prove Atomic Formula Logic Theory
Unable to display preview. Download preview PDF.
- Loveland, D.W. (1984), Automated theorem proving: a quarter-century review, in Automated Theorem Proving (Bledsoe and Loveland, eds.), American Mathematical Society, Providence, RI, pp. 1–45.Google Scholar
- Newell, A., Shaw, J.C., and Simon, H.A. (1956), Empirical explorations of the logic theory machine: A case study in heuristics. Proceedings of the Western Joint Computer Congress, 1956, pp. 218–239. Also in Computers in Thought (Fie-genbaum and Feldman, eds.), McGraw-Hill New York, 1963, pp. 134–152. Page numbers cited are from this reference.Google Scholar
- O’Leary, D.J. (1984), The Propositional Logic of Principia Mathematica, and Some of its Forerunners. Presented at the Russell Conference, 1984, Trinity College, University of Toronto. Unpublished.Google Scholar
- Russell, B. (1956), Letter to Herbert Simon dated 2 November 1956. Located at the Russell Archives, McMaster University.Google Scholar
- Simon, H. (1956) Letter to Bertrand Russell dated 9 September 1957. Located at the Russell Archives, McMaster University.Google Scholar
- Tiernay, P. (1983), Herbert Simon’s simple economics. Science 83,4, No. 9, November 1983.Google Scholar
- Wang, H. (1960), Toward mechanical mathematics, IBM J. Res. Develop., 1960, 2–22. Also in Logic, Computers and Sets, Chelsea, New York, 1970.Google Scholar