Principia Mathematica and the Development of Automated Theorem Proving
Daniel J. O’Leary · Birkhäuser Boston eBooks · 2008
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. 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.