📄 The logic theory machine: A complex information processing system

Summary

Note: The supplied PDF extraction contains only empty page markers (pp. 1–64) and no text. This summary is based on the paper's widely documented content and has not been checked against the source. Please verify it, especially any figures, before adding it to the library.

Newell and Simon ask whether a machine can solve problems that people solve through insight and trial-and-error rather than a guaranteed procedure. Their test domain is proving theorems of sentential logic as in Whitehead and Russell's Principia Mathematica. They specify the Logic Theory Machine (Logic Theorist, LT), a program that starts from the Principia axioms and previously proved theorems. Instead of enumerating all possible proofs (the exhaustive "British Museum" approach), LT uses heuristic methods: substitution, detachment and chaining. These methods mostly work backward from the target theorem, guided by similarity tests between expressions. The authors describe the system in an information-processing (list-based) language and report that it finds proofs for many Chapter 2 theorems. The work matters because it introduced heuristic search, list processing and symbolic problem solving as a computational model of human thinking. It is often cited as the first artificial intelligence program.

Key points

• Domain: propositional calculus from Principia Mathematica, Chapter 2, starting from its five basic axioms.
• Methods: substitution, detachment, and forward/backward chaining, used heuristically rather than as an exhaustive algorithm.
• Implementation: a list-processing information language (IPL lineage), associated with RAND's JOHNNIAC computer. J. C. Shaw also contributed to the project.
• Commonly cited result: proofs for 38 of the first 52 Chapter 2 theorems. This figure is usually traced to the follow-up "Empirical Explorations" paper (1957), so check it against this text.
• Significance: presented at the 1956 Dartmouth-era meetings; it laid the groundwork for heuristic search and cognitive simulation in AI.