Logic Theorist
The Logic Theorist was a computer program written in 1955–56 by Allen Newell, J. Clifford Shaw and Herbert Simon at RAND and Carnegie Tech that proved theorems of propositional logic from Whitehead and Russell's Principia Mathematica. It is often called the first artificial intelligence program, a description that is arguable but reflects its role: it was the first widely noted demonstration that a machine could carry out a task that people regarded as requiring reasoning, using methods that resembled human heuristics rather than brute-force computation.
Its headline result was a modest, well-defined one. Given the axioms of the propositional calculus in Principia, the program proved 38 of the first 52 theorems of Chapter 2, and for at least one of them it found a proof that was shorter or more elegant than the one given by Whitehead and Russell. The work was described by Newell and Simon in The Logic Theory Machine, published in the IRE Transactions on Information Theory in September 1956, and presented at the Dartmouth summer workshop that year, where it was the one working program that most attendees could point to. Before it ran on a real machine, the design had been checked by hand, with participants acting out the program's steps, which demonstrated that the procedure was precise enough to be a program at all.
The method was heuristic search through proofs, working backward from the goal. A theorem to be proved was treated as a node in a search tree. The program applied three kinds of inference: substitution, which instantiates a variable in a known theorem; detachment, which is modus ponens; and chaining, which links implications. It selected promising steps by rules of thumb rather than enumerating every derivation, which the authors contrasted with the exhaustive British Museum algorithm, generating all possible proofs, a method that would be hopelessly slow because the number of candidates explodes. The program also kept a list of theorems already proved and tried them as lemmas, so it was a learning-free but memory-using system.
The programming language created for it, Information Processing Language, or IPL, may have mattered more than the theorems. Written because ordinary machine code could not express the program's flexible structures, IPL introduced list processing, in which data are chained collections of symbols that grow, shrink and share parts while a program runs, along with hierarchical subroutines and dynamic memory allocation. It was used on RAND's JOHNNIAC computer. John McCarthy, who saw IPL at Dartmouth, was impressed by list processing but found the language itself low-level, and designed Lisp (specified in 1958) to put those ideas on a cleaner mathematical footing, which is how the Logic Theorist's technical legacy reached most of AI.
There are several pitfalls in how it is described. It worked only in the propositional calculus, with a handful of axioms and a comparatively small search space, and its behavior did not generalize without more engineering; 38 of 52 also means 14 theorems were not proved within its resource limits. Calling it the first AI program is a judgment, since earlier game-playing programs such as Christopher Strachey's checkers in 1951 and Dietrich Prinz's chess program existed, but these were not framed as models of reasoning. And its purpose, to Newell and Simon, was psychology as much as engineering: they argued that its heuristics modeled how people prove things, though the later comparisons with people's reports were done with the successor, the General Problem Solver.
Modern descendants are numerous. Automated theorem provers and interactive proof assistants such as Lean, Coq and Isabelle rely on search over proof steps, with heuristics that choose among them, and recent systems pair a learned model that proposes steps with a formal checker that guarantees correctness, the same division between guided guessing and mechanical verification. The program's emphasis on subgoals and stored lemmas persists in modern reasoning-oriented systems, and the reminder that a search tree needs good pruning is still the central issue.
Read the Logic Theorist as the first proof that reasoning-like behavior could be programmed as guided search over symbols: a narrow success, 38 theorems in one small logic, whose methods and whose language, IPL, shaped what AI looked like for the next generation.