What was the Logic Theorist, often called the first AI program?

Before anyone had agreed on the phrase "artificial intelligence," two researchers and a programmer set out to make a computer do something that seemed to need real thought: prove theorems in logic. The result, the Logic Theorist, could take a statement from one of the most famous mathematics books of the twentieth century and find a chain of steps that showed it was true.

What made it remarkable was not raw speed. It was the strategy. Instead of grinding through every possible combination, the program worked a little like a student at a blackboard: it looked at what it needed to prove, noticed resemblances to things it already knew, and tried the most promising moves first.

Who built it, and when

The team was Allen Newell, a young researcher at the RAND Corporation in Santa Monica, California; Herbert A. Simon, a professor at the Carnegie Institute of Technology in Pittsburgh who consulted at RAND; and J. C. "Cliff" Shaw, a RAND programmer. Newell and Simon began work in 1955. By January 1956 the design was far enough along that Simon told a class, "Over Christmas, Al Newell and I invented a thinking machine."

No computer was free to run it yet, so they tested it by hand. Simon gathered his wife, his three children and some graduate students, gave each person a card describing one piece of the program, and had them act out its steps together. Shaw then did the hard work of making it run on RAND's JOHNNIAC computer.

The formal description came in a RAND paper by Newell and Simon dated July 12, 1956, titled "The Logic Theory Machine." They presented it on September 10, 1956, at a symposium of the Institute of Radio Engineers held at MIT in Cambridge, Massachusetts. That summer they had also shown the program at the Dartmouth workshop on artificial intelligence, where, by most accounts, the other participants were less impressed than its makers expected.

What problem it tackled

The theorems came from Principia Mathematica, the vast work in which Alfred North Whitehead and Bertrand Russell tried to rebuild mathematics from pure logic. Its second chapter starts from five axioms, statements taken as true, and derives dozens of theorems from them using a few rules:

Substitution: in a true statement, you may replace a variable everywhere with any expression.
Detachment: if "A" is true and "A implies B" is true, then B is true.
Replacement: you may swap an expression for its definition, for example "p implies q" for "not-p or q."

A proof is just a list of statements, each one an axiom, an earlier theorem, or the result of applying one of these rules.

How it worked

In principle a computer could find any proof by brute force: build every statement reachable in one step, then two, then three, and wait for the target to appear. Newell and Simon showed why that fails. If each step can continue in ten ways, there are already 10,000 chains four steps long. A search that blindly picks among them expects to try about 5,000. But if clues let the program discard eight of the ten options at each step, only 16 four-step chains remain.

Those clues are heuristics: rules of thumb that often work but carry no guarantee. The paper draws a sharp line between algorithms, systematic procedures that are certain to finish, and heuristic methods, which are faster and more human. The Logic Theorist had several:

Method	What it tries	Everyday analogy
Substitution	Find a known theorem that looks like the goal, then make the two match	Spotting that a new puzzle is an old one with different labels
Detachment	Find a theorem "B implies goal," then set "prove B" as a new subproblem	"To get into the house, I need the key; so where is the key?"
Chaining	Link "A implies B" and "B implies C" to reach "A implies C," forward or backward	Planning a trip through a connecting city

All of them work backward from the goal. Each method can create smaller problems, which the program stores and attacks in turn. The paper's own worked example proves theorem 2.01 in three steps: start from axiom 1.2, substitute "not-p" for p, then apply a definition.

To build all this, the team also created a new kind of programming language, IPL (Information Processing Language), which stored data as linked lists that could grow and change while the program ran. That was unusual for computers built mainly to crunch numbers.

Try it: Take the statement "if it rains, the street is wet; if the street is wet, cars slow down." Write the conclusion you can chain from these two lines, then explain in one sentence which step was "working backward" if you started from "cars slow down."

Why it mattered

The Logic Theorist eventually found proofs for 38 of the 52 opening theorems of Principia's second chapter. For theorem 2.85 it found a proof shorter and neater than the one Whitehead and Russell had published, and Simon showed it to Russell, who was reportedly delighted. An attempt to publish that proof in The Journal of Symbolic Logic was turned down.

Its larger importance lay in three ideas. It treated a computer as a machine for manipulating symbols, not only numbers. It showed that search guided by heuristics could solve problems that brute force could not. And it was offered as a model of how people think, launching the study of thinking as information processing. Newell and Simon went straight on to a broader successor, the General Problem Solver, and the list-processing idea behind IPL fed into John McCarthy's Lisp language.

How does the Logic Theorist's idea of heuristic search show up in AI today?

Almost every system that has to choose among many options still relies on the bargain the Logic Theorist made: give up the guarantee of trying everything in exchange for a good chance of finding an answer quickly. A route planner on your phone does not test every road in the country; it uses an estimate of remaining distance to focus on promising streets. Chess and Go programs prune the moves that look hopeless so they can look deeper at the rest.

What has changed is where the rules of thumb come from. In 1956, Newell and Simon wrote them by hand, based on their own sense of how they solved problems. Many current systems learn their guidance from data instead. DeepMind's game programs, for example, train a neural network to judge which moves and positions look good, then use that judgment to steer a search.

Automated theorem proving also continues as its own field. Programs now help check proofs in mathematics and verify that computer chips and software behave as designed. They are far more powerful than the Logic Theorist, but the basic picture is the same: a goal, a set of rules, and a search that has to be clever about where to look.