Logic TheoristLogic Theorist

In late 1955, Allen Newell, Herbert Simon, and programmer Cliff Shaw built a program designed to prove theorems in symbolic logic. Simon famously told his students that over Christmas he and Newell had invented a thinking machine. The Logic Theorist, running on RAND's JOHNNIAC computer, is widely considered the first artificial intelligence program.

The program worked through the theorems of Whitehead and Russell's Principia Mathematica, the monumental attempt to ground all of mathematics in logic. It eventually proved 38 of the first 52 theorems in chapter two. For one of them, theorem 2.85, it found a proof shorter and more elegant than the one Russell and Whitehead had published.

Simon wrote to Bertrand Russell about the machine's improvement on his proof, and Russell replied with delight. But when Newell and Simon submitted a paper on the new proof to the Journal of Symbolic Logic, listing the Logic Theorist as a co-author, the journal declined it. A novel proof of an already-proven theorem was not deemed noteworthy, whoever or whatever found it.

Under the hood, the Logic Theorist introduced ideas that would define decades of AI: representing problems as trees to be searched, and using heuristics, rules of thumb, to prune paths unlikely to succeed. Since exhaustive search was hopeless even for simple logic, intelligence had to mean searching selectively.

Newell and Simon presented the program at the Dartmouth workshop in 1956, giving the newly named field its first working exhibit. They went on to build the General Problem Solver and to articulate the physical symbol system hypothesis, the claim that symbol manipulation is sufficient for intelligence, which anchored the symbolic tradition for thirty years.