The Logic Theorist (LT) is a program that proves theorems of propositional logic. Allen Newell, Herbert Simon and Cliff Shaw wrote it at the RAND Corporation in 1955–1956, and it is usually presented as the first artificial intelligence program: a machine that does not compute numbers but manipulates symbols to find proofs (Newell & Simon, 1956). It is the type specimen of what Haugeland (1985) would later dub GOFAI, "good old-fashioned" symbolic AI.
How it works
LT receives the five propositional axioms of Whitehead and Russell's Principia Mathematica (*1.2 to *1.6), a few definitions, and a theorem from chapter 2 to prove. It has few methods: substitution (instantiating the variables of a known axiom or theorem until it matches the goal), detachment (modus ponens: if I want B and I have A → B, it is enough to prove A) and chaining, forward or backward. For instance, *2.01, (p → ¬p) → ¬p, follows from *1.2, (p ∨ p) → p, by substituting ¬p for p and rewriting ¬p ∨ ¬p as p → ¬p by definition.
Each method that fails to close the proof leaves subproblems on a list, which the program works through until it finds a proof or exhausts an effort limit. This is heuristic search: enumerating every sequence of formulas until one is a proof is possible in principle and absurd in practice; working backward from the goal prunes that space at the price of guaranteeing nothing. Every proved theorem, moreover, goes into memory and serves as a premise for the next ones.
According to Newell et al. (1957), LT proved 38 of the first 52 theorems of chapter 2 and, for *2.85, found a shorter proof than the one in Principia. Simon showed it to Russell, who, as Simon told the story, replied with delight.
Where it appeared
Newell and Simon came to the Dartmouth workshop in the summer of 1956 with the program already specified and hand-simulated (Shrager, 2026), something almost nobody else had. Mitchell recounts that the field's future "big four", McCarthy, Minsky, Newell and Simon, met there and came away with tremendous optimism (M. Mitchell, 2019, ch. 1). On September 11 of that year, LT opened the second day of the MIT Symposium on Information Theory; that same day Noam Chomsky presented "Three models for the description of language", and both papers appeared in the same issue of the IRE Transactions on Information Theory. George Miller (2003) dates the conception of cognitive science to that day: symbolic AI and generative grammar were presented in the same room.
What it left behind
To program LT, the team invented IPL, a language of lists, symbols and recursion that is a direct ancestor of Lisp (Shrager, 2026). Its heuristics were generalized in the General Problem Solver, which solved puzzles such as Missionaries and Cannibals (M. Mitchell, 2019, ch. 1), and later specialized in expert systems, which traded general search for many domain rules. The idea of searching a tree with good heuristics runs all the way to Deep Blue and AlphaGo. Philosophically, LT was, in retrospect, an early proof of concept for what Newell and Simon would later call the physical symbol system hypothesis (Newell & Simon, 1976).
Limits
LT only knows a small, decidable fragment of logic, and its hand-written heuristics do not learn. Mitchell points out a trait of the whole family: replace MISSIONARIES with "Z372B" and the program works exactly the same, because for the machine the meaning of a symbol comes down to how it is combined and operated on (M. Mitchell, 2019, ch. 1). Today's reasoning models invert the recipe: heuristics learned from data, and proofs that cannot always be audited step by step.