Logic Theorist proves its first theorems

Over Christmas 1955 Herbert Simon told his class at Carnegie Tech that he and Allen Newell had invented a thinking machine. What they had was a plan for a program, and a way of simulating it by hand with index cards passed among Simon's family. By the summer of 1956 Cliff Shaw had it running on RAND's JOHNNIAC, and the Logic Theorist was proving theorems from the second chapter of Russell and Whitehead's Principia Mathematica. It eventually proved 38 of the first 52, and found a proof of theorem 2.85 shorter than the one in the book. The Journal of Symbolic Logic declined to publish it with the program as co-author.

The technique was search with heuristics. Rather than grind through every possible derivation, the program worked backwards from the goal, chose substitutions that looked promising, and pruned the rest. Newell and Simon called the search space a tree and the pruning rules heuristics, and both words stuck.

Logic Theorist was demonstrated at the Dartmouth workshop that summer, where it was the only actual working system in the room. It set the pattern for two decades: intelligence as symbol manipulation, reasoning as search, and the neuron nowhere in sight.