Logic Theorist is a computer program written in 1956 byAllen Newell,Herbert A. Simon, andCliff Shaw.^[1] It was the first program deliberately engineered to performautomated reasoning, and has been described as "the firstartificial intelligence program".^[1][a] Logic Theorist proved 38 of the first 52 theorems in chapter two ofWhitehead andBertrand Russell'sPrincipia Mathematica, and found new and shorter proofs for some of them.^[3]

In 1955, when Newell and Simon began to work on the Logic Theorist, the field ofartificial intelligence did not yet exist; the term "artificial intelligence" would not be coined until the following summer.^[b]

Simon was apolitical scientist who had previously studied the way bureaucracies function as well as developing his theory ofbounded rationality (for which he would later win theNobel Memorial Prize in Economic Sciences in 1978). He believed the study of business organizations requires, like artificial intelligence, an insight into the nature of human problem solving anddecision making. Simon has stated that when consulting atRAND Corporation in the early 1950s, he saw a printer typing out a map, using ordinary letters and punctuation as symbols. This led him to think that a machine that could manipulate symbols could simulate decision making and possibly even the process of human thought.^[5][6]

The program that printed the map had been written by Newell, a RAND scientist studying logistics andorganization theory. For Newell, the decisive moment was in 1954 whenOliver Selfridge came to RAND to describe his work onpattern matching. Watching the presentation, Newell suddenly understood how the interaction of simple, programmable units could accomplish complex behavior, including the intelligent behavior of human beings. "It all happened in one afternoon," he would later say.^[2][7] It was a rare moment of scientific epiphany.

"I had such a sense of clarity that this was a new path, and one I was going to go down. I haven't had that sensation very many times. I'm pretty skeptical, and so I don't normally go off on a toot, but I did on that one. Completely absorbed in it—without existing with the two or three levels consciousness so that you're working, and aware that you're working, and aware of the consequences and implications, the normal mode of thought. No. Completely absorbed for ten to twelve hours."^[8]

Newell and Simon began to talk about the possibility of teaching machines to think. Their first project was a program that could prove mathematical theorems like the ones used inBertrand Russell andAlfred North Whitehead'sPrincipia Mathematica. They enlisted the help of computer programmerCliff Shaw, also from RAND, to develop the program. (Newell says "Cliff was the genuine computer scientist of the three".^[9])

The first version was hand-simulated: they wrote the program onto 3x5 cards and, as Simon recalled:

In January 1956, we assembled my wife and three children together with some graduate students. To each member of the group, we gave one of the cards, so that each one became, in effect, a component of the computer program ... Here was nature imitating art imitating nature.^[10]

They succeeded in showing that the program could successfully prove theorems as well as a talented mathematician. Eventually Shaw was able to run the program on the computer at RAND's Santa Monica facility.

In the summer of 1956,John McCarthy,Marvin Minsky,Claude Shannon andNathan Rochester organized a conference on the subject of what they called "artificial intelligence" (a term coined by McCarthy for the occasion). Newell and Simon proudly presented the group with the Logic Theorist. It was met with a lukewarm reception.Pamela McCorduck writes "the evidence is that nobody save Newell and Simon themselves sensed the long-range significance of what they were doing."^[11] Simon confides that "we were probably fairly arrogant about it all"^[12] and adds:

They didn't want to hear from us, and we sure didn't want to hear from them: we had something toshow them! ... In a way it was ironic because we already had done the first example of what they were after; and second, they didn't pay much attention to it.^[13]

Logic Theorist soon proved 38 of the first 52 theorems in chapter 2 of thePrincipia Mathematica. The proof of theorem 2.85 was actually more elegant than the proof produced laboriously by hand by Russell and Whitehead. Simon was able to show the new proof to Russell himself who "responded with delight".^[3] They attempted to publish the new proof inThe Journal of Symbolic Logic, but it was rejected on the grounds that a new proof of an elementary mathematical theorem was not notable, apparently overlooking the fact that one of the authors was a computer program.^[14][3]

Newell and Simon formed a lasting partnership, founding one of the first AI laboratories at theCarnegie Institute of Technology and developing a series of influential artificial intelligence programs and ideas, including theGeneral Problem Solver,Soar, and theirunified theory of cognition.

The Logic Theorist is a program that performs logicalprocesses on logicalexpressions.^[15] The Logic Theorist operates on the following principles:

• An expression is made ofelements.
• There are two kinds of memories:working andstorage.
• Each working memory contains a single element. The Logic Theorist usually uses 1 to 3 working memories.
• Each storage memory is a list representing a full expression or a set of elements. In particular, it contains all the axioms and proven logical theorems.
• An expression is anabstract syntax tree, each node being an element with up to 11 attributes.

For example, the logical expression${\displaystyle \mathrm{\neg }P\to (Q\wedge \mathrm{\neg }P)}$ is represented as a tree with a root element representing${\displaystyle \to }$. Among the attributes of the root element are pointers to the two elements representing the subexpressions${\displaystyle \mathrm{\neg }P}$ and${\displaystyle Q\wedge \mathrm{\neg }P}$.

There are four kinds of processes, from the lowest to the highest level.

• Instruction: These are similar toassembly code. They may either perform a primitive operation on an expression in working memory, or perform a conditional jump to another instruction. An example is "put the right sub-element of working-memory 1 to working-memory 2"
• Elementary process: These are similar tosubroutines. A sequence of instructions that can be called.
• Method: A sequence of elementary processes. There are 4 methods:
  • substitution: given an expression, it attempts to transform it to a proven theorem or axiom by substitutions of variables and logical connectives.
  • detachment: given expression${\displaystyle B}$, it attempts to find a proven theorem or axiom of form${\displaystyle A\to B^{\prime }}$, where${\displaystyle B^{\prime }}$ yields${\displaystyle B}$ after substitution, then attempts to prove${\displaystyle A}$ by substitution.
  • chaining forward: given expression${\displaystyle A\to C}$, it attempts to find for a proven theorem or axiom of form${\displaystyle A\to B}$, then attempt to prove${\displaystyle B\to C}$ by substitution.
  • chaining backward: given expression${\displaystyle A\to C}$, it attempts to find for a proven theorem or axiom of form${\displaystyle B\to C}$, then attempt to prove${\displaystyle A\to B}$ by substitution.
• executive control method: This method applies each of the 4 methods in sequence to each theorem to be proved.

Logic Theorist introduced several concepts that would be central to AI research:

Reasoning as search

Logic Theorist explored asearch tree: the root was the initialhypothesis, each branch was a deduction based on the rules of logic. Somewhere in the tree was the goal: theproposition the program intended to prove. The pathway along the branches that led to the goal was aproof – a series of statements, each deduced using the rules of logic, that led from the hypothesis to the proposition to be proved.

Heuristics

Newell and Simon realized that thesearch tree would growexponentially and that they needed to "trim" some branches, using "rules of thumb" to determine which pathways were unlikely to lead to a solution. They called thesead hoc rules "heuristics", using a term introduced byGeorge Pólya in his classic book onmathematical proof,How to Solve It. (Newell had taken courses from Pólya atStanford).^[16] Heuristics would become an important area of research inartificial intelligence and remains an important method to overcome theintractablecombinatorial explosion of exponentially growing searches.

List processing

To implement Logic Theorist on a computer, the three researchers developed a programming language,IPL, which used the same form of symbolic list processing that would later form the basis of McCarthy'sLisp programming language, an important language still used by AI researchers.^[17][18]

Pamela McCorduck writes that the Logic Theorist was "proof positive that a machine could perform tasks heretofore considered intelligent, creative and uniquely human".^[3] And, as such, it represents a milestone in the development ofartificial intelligence and our understanding of intelligence in general.

Simon told a graduate class in January 1956, "Over Christmas, Al Newell and I invented a thinking machine,"^[19][20]and would write:

[We] invented a computer program capable of thinking non-numerically, and thereby solved the venerablemind-body problem, explaining how a system composed of matter can have the properties of mind.^[21]

This statement, that machines can have minds just as people do, would be later named "Strong AI" by philosopherJohn Searle. It remains a serious subject of debate up to the present day.

Pamela McCorduck also sees in the Logic Theorist the debut of a new theory of the mind, theinformation processing model (sometimes calledcomputationalism orcognitivism). She writes that "this view would come to be central to their later work, and in their opinion, as central to understanding mind in the 20th century asDarwin's principle of natural selection had been to understanding biology in thenineteenth century."^[22] Newell and Simon would later formalize this proposal as thephysical symbol systems hypothesis.

• Crevier, Daniel (1993).AI: The Tumultuous Search for Artificial Intelligence. New York, NY: BasicBooks.ISBN 0-465-02997-3., pp. 44–46.
• McCorduck, Pamela (2004),Machines Who Think (2nd ed.), Natick, Massachusetts: A. K. Peters,ISBN 1-5688-1205-1, pp. 161–170.
• Russell, Stuart J.;Norvig, Peter. (2021).Artificial Intelligence: A Modern Approach (4th ed.). Hoboken: Pearson.ISBN 9780134610993.LCCN 20190474.

• Newell and Simon's RAND Corporation report on the Logic Theorist
• Full length version of Newell and Simon's RAND Corporation report on the Logic Theorist
• CMU Libraries: Human and Machine Minds
• Source code as PDF on Github

• History of artificial intelligence
• Theorem proving software systems

• Articles with short description
• Short description is different from Wikidata