Logic Theorist
In plain wordsA 1956 computer program that proved theorems from a classic logic textbook by searching cleverly rather than trying every possibility. Many historians count it as the first AI program.
A theorem-proving program that Allen NewellAllen Newell, prop. n.: An American computer scientist who, with Herbert Simon, wrote early AI programs that solved problems the way people do, and who sought a single theory of how the mind works., Herbert A. SimonHerbert A. Simon, prop. n.: An American scientist of decision-making who, with Allen Newell, wrote some of the first AI programs and argued that minds and computers both think by manipulating symbols. and Cliff Shaw built in 1955–1956 to find proofs for the propositional-logic theorems in chapter 2 of Whitehead and Russell's Principia Mathematica. Working backward from the theorem to be proved, it applied substitution, replacement and detachment, and used heuristicsheuristic, n.: A rule of thumb: a quick, usually good-enough way to make a decision or to estimate how close you are to a goal, without any guarantee of finding the best answer. — such as matching the goal against already-proved theorems and pursuing subproblems that looked similar — to prune an otherwise explosive search. Of the chapter's first 52 theorems it eventually proved 38, and for one of them it found a proof more elegant than the book's. The program established ideas central to symbolic AIsymbolic AI, n.: An approach to AI that writes knowledge down as human-readable symbols and rules, such as 'every bird has wings', and reasons by manipulating them step by step instead of learning patterns from data.: reasoning as heuristic search over symbol structures, and list processing, implemented in the purpose-built Information Processing Language (IPL).
The Logic Theorist was the only working program presented at the Dartmouth workshop.
Origin
Developed at the RAND Corporation and the Carnegie Institute of Technology. Newell and Simon first simulated it by hand, with family members and students acting as subroutines, before it ran on RAND's JOHNNIAC computer in 1956. It was described in their 1956 paper 'The Logic Theory Machine' and shown at the Dartmouth workshopDartmouth workshop, prop. n.: A summer meeting of scientists at Dartmouth College in 1956, planned in a 1955 funding proposal that first used the phrase 'artificial intelligence'. Most histories treat it as the moment AI became a research field of its own..
Usage note
Simon later recalled telling a class in January 1956 that over Christmas he and Newell had invented a thinking machine. A paper listing the program as a coauthor was reportedly rejected by the Journal of Symbolic Logic.
Related
- General Problem SolverGeneral Problem Solver, prop. n.: A 1950s program meant to solve any well-defined puzzle by repeatedly comparing where it was with where it wanted to be and choosing steps that closed the gap.
- symbolic AIsymbolic AI, n.: An approach to AI that writes knowledge down as human-readable symbols and rules, such as 'every bird has wings', and reasons by manipulating them step by step instead of learning patterns from data.
- heuristicheuristic, n.: A rule of thumb: a quick, usually good-enough way to make a decision or to estimate how close you are to a goal, without any guarantee of finding the best answer.
- automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement.
- Dartmouth workshopDartmouth workshop, prop. n.: A summer meeting of scientists at Dartmouth College in 1956, planned in a 1955 funding proposal that first used the phrase 'artificial intelligence'. Most histories treat it as the moment AI became a research field of its own.
- physical symbol system hypothesisphysical symbol system hypothesis, n.: The 1976 claim by two AI pioneers that a machine which stores and rearranges symbols according to rules has everything needed for general intelligence, and that anything generally intelligent must be such a machine.
Sources
- Newell, A. & Simon, H. A. (1956). The Logic Theory Machine: A Complex Information Processing System. IRE Transactions on Information Theory IT-2(3), 61–79.
Mentioned in
symbolic AIsymbolic AI, n.: An approach to AI that writes knowledge down as human-readable symbols and rules, such as 'every bird has wings', and reasons by manipulating them step by step instead of learning patterns from data., Allen NewellAllen Newell, prop. n.: An American computer scientist who, with Herbert Simon, wrote early AI programs that solved problems the way people do, and who sought a single theory of how the mind works., automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement., backward chainingbackward chaining, n.: A way of reasoning that starts from the question ('is this true?') and works backward, looking for rules that would prove it and then checking whether their conditions hold., Dartmouth workshopDartmouth workshop, prop. n.: A summer meeting of scientists at Dartmouth College in 1956, planned in a 1955 funding proposal that first used the phrase 'artificial intelligence'. Most histories treat it as the moment AI became a research field of its own., General Problem SolverGeneral Problem Solver, prop. n.: A 1950s program meant to solve any well-defined puzzle by repeatedly comparing where it was with where it wanted to be and choosing steps that closed the gap., Herbert A. SimonHerbert A. Simon, prop. n.: An American scientist of decision-making who, with Allen Newell, wrote some of the first AI programs and argued that minds and computers both think by manipulating symbols., heuristicheuristic, n.: A rule of thumb: a quick, usually good-enough way to make a decision or to estimate how close you are to a goal, without any guarantee of finding the best answer., reasoningreasoning, n.: Working out conclusions step by step from facts, rules or evidence, as in solving a math problem or planning a trip. Whether today's AI truly reasons, or imitates reasoning, is debated., RAND CorporationRAND Corporation, prop. n.: An American research organization, long funded mainly by the US government, where early AI programs were written and which now advises governments on AI and security.