*Principia Mathematica* and the Development of Automated Theorem Proving

Chapter

## Abstract

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.

## Keywords

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.

## Preview

Unable to display preview. Download preview PDF.

## Bibliography

- 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 - Whitehead, A.N. and Russell, B. (1935),
*Principia Mathematica*, 2nd ed., Cambridge University Press, Cambridge, UK.MATHGoogle Scholar

## Copyright information

© Birkhäuser Boston 2008