Logic Theorist: Rules of thumb prove theorems

The event and the narrow claim

On June 15, 1956, the RAND Corporation issued report P-868, "The Logic Theory Machine: A Complex Information Processing System," by Allen Newell and Herbert A. Simon. It specified a program the authors called the logic theorist, or LT, that searched for proofs of theorems in the propositional calculus of Whitehead and Russell's Principia Mathematica. The original June date is recorded in Jeremy Norman's history of the program; RAND's own record of P-868 preserves a revised issue dated July 12, 1956. The paper was presented to the Institute of Radio Engineers' Professional Group on Information Theory at MIT that September and printed in the September issue of IRE Transactions on Information Theory. J. C. Shaw, the RAND programmer who would realize the design on a computer, appears in a footnote as the authors' partner, not on the byline.

The documented claim of the 1956 report is modest and exact. It describes a system that relies on heuristic methods similar to those observed in human problem solving, in contrast to the systematic algorithms that computers ordinarily ran, and it states that the paper concerns only the specification of the system, not its realization in a computer. It even notes that LT was small enough to be hand simulated, barely. The famous performance figures came later, from machine runs published in February 1957. The larger judgment, that LT was the first artificial intelligence program and the seed of symbolic AI and of computer models of thinking, is retrospective. Part of it is well supported, part of it is contested, and all of it should be kept apart from what the June 1956 report itself demonstrated.

From chess to logic between Pittsburgh and Santa Monica

Simon had met Newell at RAND in 1952, and in about 1954 the two concluded that the right way to study human problem solving was to simulate it with computer programs, as Simon recalled in his Nobel autobiography. His memoir of Newell for the National Academy of Sciences dates Newell's commitment to September 1954, when Oliver Selfridge described a running pattern-recognition program at a RAND seminar. Newell then designed a humanlike chess program, presented in March 1955, and moved to Pittsburgh early that year as RAND's one-person outpost to work with Simon at the Carnegie Institute of Technology, with Shaw collaborating from Santa Monica and the program destined for RAND's JOHNNIAC computer.

The target changed twice. In Simon's account, chess gave way to geometry and geometry to logic, and the Logic Theory Machine emerged as a hand simulation by December 15, 1955. The choice of Principia was practical rather than philosophical. Simon later wrote, in a passage quoted by Norman, that the system was based on Principia largely because a copy happened to be on his bookshelf, and that the point was to show a computer could find solutions in a complex nonnumerical domain, not to contribute to logic. Before any machine ran it, the team executed the program by hand, with family members and students each acting as a component. Edward Feigenbaum, then a student in Simon's class, later recalled Simon announcing in January 1956, "Over Christmas Allen Newell and I invented a thinking machine," as quoted in Jeff Shrager's 2026 reconstruction of the program.

How the logic theorist searched

The task, as the RAND report sets it out, is purely formal. LT starts from the five axioms of Principia's propositional calculus, numbered 1.2 to 1.6, and three rules. Substitution puts any expression in place of a variable throughout a true expression. Replacement swaps "p implies q" for its definition, "not-p or q," and back. Detachment yields B from A and "A implies B." A proof is a sequence of expressions, each an axiom, a known theorem or a product of earlier lines. The report's first worked example is theorem 2.01, "(p implies not-p) implies not-p": substitute not-p for p in axiom 1.2, "(p or p) implies p," then replace the resulting "not-p or not-p" with "p implies not-p."

What made LT a problem solver rather than an enumerator was the order in which it looked. It worked backward from the expression to be proved. Its substitution method considered only axioms and theorems that resembled the target, using a similarity test that compared counts of levels and variables, and then tried to match a candidate to the target piece by piece, substituting variables and replacing connectives as it went. Its detachment method looked for a known theorem of the form "A implies B" whose right side matched the target, and set up A as a new subproblem. Its chaining methods used the transitivity of implication, forward and backward, to create subproblems the same way. An executive routine tried the methods in turn, kept unsolved subproblems on a list, chose the simplest one next, discarded duplicates, and gave up when a tally of attempted substitutions passed a fixed work limit.

Two further features mattered. Every theorem LT proved was stored and became material for later proofs, which the report calls its one important form of learning; without it, the authors doubted LT would prove more than the first few theorems of the chapter. And the report made the economics of search concrete. If each proof chain could be continued ten ways, there would be ten thousand chains four steps long, but cues that eliminated eight of the ten continuations at each step would leave only sixteen to examine. Section III of the report printed the complete program.

The case for heuristics and the British Museum algorithm

The February 1957 paper, Empirical Explorations of the Logic Theory Machine, presented at the Western Joint Computer Conference in Los Angeles and now signed by Newell, Shaw and Simon, made the argument explicit. It defined an algorithm as a process guaranteed to produce a solution eventually, and a heuristic as one that may solve a problem but offers no guarantee. Its illustration was a combination safe: trying every combination is an algorithm, yet slow enough that a safe still protects valuables from people who know it.

To show why proving theorems was hard, the authors built a deliberately naive foil they named the British Museum algorithm, which generates every possible proof in order of length, discarding duplicates and checking whether the last line is the target. Theorem 2.02 was the 79th theorem it produced, after about 158 seconds, while LT proved the same theorem by substitution in about 10 seconds. For the theorems that required detachment, the authors estimated, the algorithm would need hundreds of thousands of years to cover Chapter 2. The 1956 report had already acknowledged that systematic decision methods for this logic existed and had even been built in hardware, the Kalin-Burkhart logic machine, so LT was framed from the start as a contrast between algorithmic and heuristic ways of doing the same task.

The numbers, stated precisely

The runs took place on the JOHNNIAC, RAND's machine based on the Princeton Institute for Advanced Study design, completed in 1954. According to the 1958 paper in Psychological Review, it had 4,096 words of magnetic core memory, 9,216 words on drums, and ran about 15,000 operations per second. Memory limits restricted the main test to the first 52 of the 67 theorems in Chapter 2. LT found proofs for 38 of them, 73 percent. Seventeen were one-step proofs by substitution, nineteen took two steps (twelve by detachment followed by substitution, seven by forward chaining followed by substitution), and two took three. Of the fourteen failures, most ended on time or memory limits. The authors knew LT could never prove one of them, theorem 2.13, and believed the same of another.

Individual timings show the shape of the search. Theorem 2.01 took about 10 seconds. Theorem 2.45, with all earlier theorems available, took about 12 minutes. After about 23 minutes LT reported that it could not prove 2.31, having run out of subproblems. The Psychological Review paper adds that about half the proofs took under a minute, most of the rest one to five minutes, and a few between 15 and 45 minutes, with time rising sharply for each additional proof step. It also reports a telling experiment. Stripped of the earlier theorems, LT failed on theorem 2.12, but given theorem 2.03 as a single hint it found a three-step proof in fifteen minutes.

One caution belongs with these figures. The 1957 paper says LT was given all earlier theorems of the chapter whether or not it had proved them itself, while the 1958 paper describes a run in which each theorem was stored only as LT proved it. Both report 38 of 52, so the headline survives, but the two descriptions of the setup are not identical. Either way, the result measures one program on one ordered list of textbook theorems, not a general ability to prove.

When it ran, and who saw it

The surviving record does not pin down the first machine proof. In his memoir of Newell, Simon dated a running program to the summer of 1956. John McCarthy recalled in his history of Lisp that at the Dartmouth summer project Newell, Shaw and Simon described IPL 2, a list-processing language for the JOHNNIAC in which they had implemented the Logic Theorist. Yet the July 1956 report says it covers only the specification and that Shaw's computer realization would be reported in later papers, and Shrager's reconstruction, while opening with the popular story of a running program at Dartmouth, argues in its historical section that machine proofs came with the IPL-II implementation in late 1956 and early 1957. What is certain is that the counted results were published in February 1957. LT's place at the Dartmouth workshop is best described as a specified design with hand-simulated results, possibly already partly running, brought by two visitors rather than produced by the meeting.

Its wider debut came at MIT. The cover of the revised report records its presentation on September 10, 1956. George Miller, who attended, later recalled Newell and Simon's "logic machine" opening the symposium's second day, September 11, the date he chose as the moment of conception of cognitive science, on a program that also included Nathaniel Rochester's IBM group and Noam Chomsky. The one-day difference between the cover and Miller's memory is minor, but it is a reminder that founding dates are partly built in retrospect.

Simon also sent the work to one of its subjects. The Bertrand Russell Archives at McMaster University record that Simon mailed the Logic Theory Machine paper to Russell on October 2, 1956, and that Russell replied on November 2 that he was quite willing to believe everything in deductive logic could be done by a machine. In September 1957 Simon sent the two 1957 papers, and Russell's reply of September 21, 1957 is catalogued as delighted with the proof-testing computer. A widely repeated detail, that LT found a shorter proof of theorem 2.85 than the one in Principia and that this was what delighted Russell, rests on Pamela McCorduck's later history as relayed by Shrager. The 1957 results paper reports only on the first 52 theorems and does not mention it, so it is treated here as unconfirmed by the primary record.

List processing: the infrastructure it forced into existence

LT needed data that grew and shrank unpredictably: expressions, lists of subproblems, descriptions of expressions. No existing language handled such structures, so the team built one. The companion 1957 paper by Newell and Shaw, Programming the Logic Theory Machine, describes it. Each element fit in one 40-bit JOHNNIAC word, lists were linked by addresses, and a single available-space list supplied new cells and took back erased ones. Hierarchies of routines 13 or 14 levels deep were common. The authors admitted the language was very costly in memory and time, and reported about fifty hours of machine computation with it.

These Information Processing Languages, IPL I to IPL V, are described in Simon's memoir as the first list-processing languages for computers. McCarthy's account shows both their influence and the divergence that followed. He took list processing but not IPL's form, which was tied to a JOHNNIAC loader, preferring to write programs algebraically, and in implementing Lisp he rejected IPL's explicit erasure in favor of garbage collection. The 1975 ACM Turing Award citation for Newell and Simon, printed with their Turing lecture, called them apparently the inventors of list processing and credited the early collaboration with Shaw at RAND. The IEEE Computer Society's biography of Shaw places him at the center of that language work and of the later JOHNNIAC Open-Shop System.

The honest limits

The sharpest criticism came from a logician. Hao Wang, in Toward Mechanical Mathematics, reported programs he wrote at IBM's Poughkeepsie laboratory in the summer of 1958 for an IBM 704. His proof procedure for the propositional calculus proved over 200 theorems from the first five chapters of Principia in about 37 minutes, of which the proving itself took under three; the 52 theorems LT attempted took under five minutes including input and output, with 2.45 in about 3 seconds and 2.31 in about 6. Wang judged it unfair to argue for heuristics by contrast with a deliberately inefficient algorithm, and suggested the plainer word "strategy." The propositional calculus is decidable, so LT had chosen a domain in which a complete mechanical method was available all along.

RAND's own later documentation was candid. Einar Stefferud's 1963 teaching version of the program said LT was not very successful compared with people or even with some other programs, and that it had survived beyond its usefulness as a research tool. The 1957 paper itself described a plateau: proofs of three steps already pressed LT against its computing limits, and the number of subproblems grew roughly exponentially with the depth of a proof.

The title of first AI program also needs qualification. Martin Davis implemented Presburger's decision procedure for arithmetic at the Institute for Advanced Study in the summer of 1954, a program that could settle only very simple statements but that a memorial account of Davis describes as producing what appears to be the first computer-generated mathematical proof. Shrager notes that Arthur Samuel's heuristic checkers program also existed before LT. What LT can claim is narrower and still significant: it was an early, fully specified program built to discover proofs by selective, humanlike search, published as a model of problem solving rather than as a calculating procedure.

The line that followed

The successors are well documented. Simon's memoir dates the extraction of means-ends analysis to the summer of 1957, from the thinking-aloud protocol of one person solving logic problems, exactly the kind of comparison between human and program that LT had opened up. That mechanism led to the General Problem Solver, published in 1960. In the 1958 Psychological Review paper the three authors presented LT as a theory of human problem solving, arguing that a program which actually finds proofs is strong evidence for the mechanisms it contains. Newell and Simon later named 1956 the critical year for information processing psychology, a judgment Miller endorsed. Their Turing lecture of 1976 traced the rudiments of best-first search to the Logic Theorist and stated the physical symbol system hypothesis, that such a system has the necessary and sufficient means for general intelligent action. That hypothesis and its companion, the heuristic search hypothesis, organized symbolic AI for a generation, and the emphasis on general methods provoked reactions such as DENDRAL, whose builders concluded that domain knowledge mattered more than general search.

LT also had a long afterlife as an artifact. After the 1962 Summer Heuristic Programming Institute at RAND, Stefferud turned Fred Tonge's IPL-V conversion of the program into a model for teaching, runnable on any computer with an IPL-V processor, including IBM's 650, 704, 709 and 7090. In 2026 Shrager wrote a new IPL-V interpreter in Common Lisp, IPL's descendant, and ran Stefferud's code, more than 99 percent of it original. It proved 16 of 23 attempted theorems from Chapter 2, which he reports as consistent with the original program's search limits.

How to place the Logic Theorist in AI history

LT is best read as the first fully documented demonstration of a research program, not as a breakthrough in logic. Its domain was decidable, its theorems were textbook exercises, and a direct algorithm soon outperformed it. What it established was a method and a stance: represent a problem as symbol structures, search the space of transformations selectively using cues, keep subproblems on lists, and treat the running program as an empirical object to be measured. The same papers that reported its successes also measured its failures, its dependence on the order of problems and the exponential growth of its search, which is part of why the work proved so generative.

Three distinctions keep the event in proportion. The June 1956 report was a specification supported by hand simulation, and the counted results came in 1957. The title of first AI program holds only under a definition that sets aside Davis's 1954 prover and Samuel's checkers player. And the long influence, through IPL, GPS, cognitive simulation and the physical symbol system hypothesis, is documented but uneven: list processing became a staple of computing, while Wang's result showed that for LT's own task a logic-based procedure was decisively faster. Recent systems that prove far harder results, such as those at the 2025 International Mathematical Olympiad, share LT's general idea of search guided by cues far more than its machinery, a connection that should be held provisionally.

References

• Newell and Simon (1956). The Logic Theory Machine: A Complex Information Processing System (RAND P-868).
• Newell and Simon (1956). The Logic Theory Machine: A Complex Information Processing System.
• Newell, Shaw and Simon (1957). Empirical Explorations of the Logic Theory Machine: A Case Study in Heuristic.
• Newell and Shaw (1957). Programming the Logic Theory Machine.
• Newell, Shaw and Simon (1958). Elements of a Theory of Human Problem Solving.
• Wang (1960). Toward Mechanical Mathematics.
• Stefferud (1963). The Logic Theory Machine: A Model Heuristic Program.
• Newell and Simon (1976). Computer Science as Empirical Inquiry: Symbols and Search.
• Simon (1997). Allen Newell, Biographical Memoirs of the National Academy of Sciences.
• Simon (1978). Herbert A. Simon: Biographical.
• McCarthy (1979). History of Lisp: LISP prehistory, Summer 1956 through Summer 1958.
• McCarthy (1979). History of Lisp: The implementation of LISP.
• Miller (2003). The cognitive revolution: a historical perspective.
• Bertrand Russell Archives (1956). Simon to Russell, 2 October 1956, enclosing The Logic Theory Machine.
• Bertrand Russell Archives (1956). Russell to Simon, 2 November 1956.
• Bertrand Russell Archives (1957). Russell to Simon, 21 September 1957.
• Norman (2026). Newell, Simon and Shaw Develop the First Artificial Intelligence Program.
• Computer History Museum (2026). JOHNNIAC.
• IEEE Computer Society (1995). John Clifford Shaw.
• Calvert, Harizanov, Omodeo, Policriti and Shlapentokh (2024). In Memory of Martin Davis.
• Shrager (2026). Executable Archaeology: Reanimating the Logic Theorist from its IPL-V Source.