O'Reilly logo

The Annotated Turing: A Guided Tour Through Alan Turing's Historic Paper on Computability and the Turing Machine by Charles Petzold

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

12  Logic and Computability

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:

images

In Wang's punched card notation this became:

images

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required