In the summer of 1958, Chinese-born logician Hao Wang took a break from his teaching duties at Oxford to log some time with a state-of-the-art IBM 704 computer at the IBM Research Laboratory in Poughkeepsie, New York. On IBM punched cards Wang encoded theorems straight out of the pages of Alfred North Whitehead and Bertrand Russell's Principia Mathematica, published almost 50 years earlier. For example, theorem *11.26 is stated in the notation of Principia Mathematica as:
In Wang's punched card notation this became:
Wang wrote three programs to read these cards and prove the encoded theorems by applying various identities and inference rules that transformed the statements back into axioms. The bulk of time spent by these programs consisted of the mechanical processes of reading the cards and printing the steps of the proof. Wang estimated that the actual processing time in proving 220 theorems from chapters *1 through *5 of Principia Mathematica was less than three minutes, and an improved version of his third program was later able to prove 158 theorems from chapters *9 through *13 in about four minutes.1
Wang's program was not the first attempt to solve theorems by computer.2 In 1954, Martin Davis used a computer built by the Institute for Advanced ...