Textbook of AI

The Logic Theorist (LT), developed by Allen Newell, Cliff Shaw and Herbert Simon in 1955–1956 jointly at the RAND Corporation in Santa Monica and the Graduate School of Industrial Administration at Carnegie Tech in Pittsburgh (now Carnegie Mellon University), is generally regarded as the first running artificial-intelligence program. It proved theorems in propositional logic from Whitehead and Russell's Principia Mathematica by heuristic search through the space of proofs, applying a small set of inference rules to known theorems and axioms in pursuit of a target formula.

LT operated by working backward from a goal formula, generating subgoals via three transformations, substitution, detachment (modus ponens) and chaining (replacing a goal with one or more antecedents), and using heuristics to prune the resulting search tree. Among the heuristics was a similarity measure that compared candidate intermediate expressions to the target formula, preferring branches that brought the proof closer to its goal. The system was implemented in IPL-II, the second incarnation of Newell, Shaw and Simon's Information Processing Language, on the JOHNNIAC vacuum-tube computer at RAND. The program exemplifies what Newell and Simon would later (1976) articulate as the Physical Symbol System Hypothesis: that intelligent action requires, and is achievable by, the manipulation of symbol structures.

Logic Theorist proved 38 of the first 52 theorems in Chapter 2 of Principia Mathematica. One of its proofs, for Theorem 2.85, was judged by Bertrand Russell to be more elegant than the one in his own book; Russell's reply to a letter from Simon announcing the result was both gracious and a touch wistful. The Journal of Symbolic Logic, however, declined to publish a paper offering Logic Theorist as a co-author with Newell, Shaw and Simon, an early skirmish in debates about machine authorship that have re-emerged in the era of large language models.

LT premiered at the 1956 Dartmouth Summer Research Project on Artificial Intelligence, the workshop that gave the field its name, and dominated discussion there. John McCarthy, Marvin Minsky, Claude Shannon and the other Dartmouth participants were presented not with a research proposal but with a working demonstration. LT introduced or codified several techniques that would become standard in symbolic AI: heuristic search as the central paradigm of problem solving; means–ends analysis in nascent form (later fully developed in the General Problem Solver, 1957); list-processing data structures for symbolic manipulation; and the use of explicit working memory holding intermediate results. Newell, Shaw and Simon's subsequent work on the General Problem Solver generalised the architecture beyond logic to a broad class of well-defined problems, and the line of work culminating in Newell's SOAR cognitive architecture in the 1980s traces directly back to Logic Theorist. Newell and Simon were jointly awarded the 1975 Turing Award for this body of work.