Principia Mathematica and the Development of Automated Theorem Proving

  • Daniel J. O’Leary


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.


Executive Director Propositional Logic Theorem Prove Atomic Formula Logic Theory 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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
  2. 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
  3. 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
  4. Russell, B. (1956), Letter to Herbert Simon dated 2 November 1956. Located at the Russell Archives, McMaster University.Google Scholar
  5. Simon, H. (1956) Letter to Bertrand Russell dated 9 September 1957. Located at the Russell Archives, McMaster University.Google Scholar
  6. Tiernay, P. (1983), Herbert Simon’s simple economics. Science 83,4, No. 9, November 1983.Google Scholar
  7. 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
  8. Whitehead, A.N. and Russell, B. (1935), Principia Mathematica, 2nd ed., Cambridge University Press, Cambridge, UK.MATHGoogle Scholar

Copyright information

© Birkhäuser Boston 2008

Authors and Affiliations

  • Daniel J. O’Leary
    • 1
  1. 1.DoverUSA

Personalised recommendations