Logic Theorist

What it was

Logic Theorist is a computer program completed in 1956 by Allen Newell, Herbert A. Simon and Cliff Shaw^[1]. Its task was formal proof: given a theorem stated in the symbolic notation of Whitehead and Russell's *Principia Mathematica*, the program searched for a chain of logical steps that would establish it. It has been described as the first program deliberately engineered to perform automated reasoning, and it has been called "the first artificial intelligence program"^[1].

Origins

Newell and Simon began work on it in 1955, when the field of artificial intelligence did not yet exist^[1]. The first version was simulated by hand: the program was written onto 3x5 cards, and in January 1956 each member of a small group — among them Simon's wife and three children — was given a card^[1]. Only later did Cliff Shaw run the program on the computer at RAND's Santa Monica facility^[1]. The work was written up as *The Logic Theory Machine: A Complex Information Processing System*, which RAND's own bibliography lists as RAND Paper P-868 of July 1956^[3].

The ideas it introduced

The Computer History Museum credits the program with bringing several critical concepts into artificial intelligence: heuristics, list processing, and reasoning as search^[2]. Heuristics are rules of thumb that cut down the number of possibilities a program has to examine — a chess program that looks only at a few plausible moves rather than every legal one is relying on a heuristic. List processing means storing information in lists whose elements can be inserted or removed as a computation proceeds, instead of in a fixed block of numbers. Reasoning as search means treating the search for a proof as movement through a space of states, from the statement to be proved toward the axioms and already established results. Together these ideas gave later work a way to talk about what a reasoning program actually does.

Results

The program proved 38 of the first 52 theorems in chapter two of *Principia Mathematica*^[1]. For Theorem 2.85 it found a new and shorter proof, which was described as more elegant than the proof Russell and Whitehead had produced by hand^[1]. Simon showed the new proof to Russell himself, who reportedly responded with delight^[1]. An attempt to publish it in *The Journal of Symbolic Logic* was rejected, on the grounds that a new proof of an elementary theorem was not notable^[1].

Reception

In the summer of 1956, Newell and Simon presented Logic Theorist at the conference organised by John McCarthy, Marvin Minsky, Claude Shannon and Nathan Rochester, where it met with a lukewarm reception^[1]. The Computer History Museum's timeline also records the project, noting that Newell, Simon and J.C. Shaw began work on a program that would eventually prove 38 theorems from *Principia Mathematica*^[2].

Where it sits

Logic Theorist belongs to the years before artificial intelligence had settled into a name and a research community: the program was built first, and the vocabulary that later described such work — heuristics, list processing, reasoning as search — was in part supplied by it^[1][2]. Its proofs were a demonstration that a machine could do something usually taken to require a mathematician's judgement, and its one clear miss — a rejected journal submission over an elementary theorem — is a reminder that the result was judged at the time as a small curiosity rather than a contribution to logic^[1].