Logic Theorist is presented at the Dartmouth summer conference

Background

In a proposal dated August 31, 1955, four researchers set out a plan for a summer project on a subject they named in the document itself. The plan called for a two-month, ten-man study of artificial intelligence during the summer of 1956 at Dartmouth College in Hanover, New Hampshire ^[2]. It was signed by J. McCarthy of Dartmouth College, M. L. Minsky of Harvard University, N. Rochester of I.B.M. Corporation and C. E. Shannon of Bell Telephone Laboratories ^[2]. Its central conjecture was that every aspect of learning or any other feature of intelligence can in principle be so precisely described that a machine can be made to simulate it ^[2]. The Rockefeller Foundation was asked to provide financial support; the total budget listed was 13,500 dollars ^[2]. McCarthy is credited with coining the phrase "artificial intelligence" for the occasion, in the text of that proposal ^[1].

The conjecture is worth reading slowly, because its emphasis falls on description rather than on machinery. It does not say that a particular machine will be built; it says that if a mental faculty can be pinned down precisely enough, then building a machine that reproduces it becomes possible in principle. The research programme that follows has two halves: first say exactly what a piece of intelligence consists of, then make it run.

The meeting

The conference itself took place in the summer of 1956, organised by McCarthy, Minsky, Shannon and Rochester ^[1]. Among the presentations was Logic Theorist, a program written by Newell and Simon ^[1].

What the program did

Logic Theorist worked in the territory of Principia Mathematica, the work on the foundations of mathematics whose theorems it took as its problems. Proving a theorem inside a formal system is a search: you begin with axioms and rules of inference and apply them a step at a time until the statement you want appears as a line of the derivation. Because every step is licensed by a rule, the whole process can be carried out by something that manipulates symbols without understanding them, which is what makes it a candidate for a machine.

By the time it was shown at Dartmouth, the program had proved 38 of the first 52 theorems in chapter two of Principia Mathematica ^[1]. It had also produced a shorter proof of Theorem 2.85, and that proof was shown to Bertrand Russell ^[1]. To a reader of the book the second result is the more surprising of the two: finding a proof at all is one thing, finding a better proof than the printed one is another.

Reception

The presentation was met with a lukewarm reception ^[1].

The two events together

The name and the demonstration belong to the same occasion. A research programme had been announced under a new label ^[1], and on the same occasion there was at least one running program to look at ^[1]. The distance between the two is the interesting part: the proposal's conjecture covers learning and every other feature of intelligence ^[2], while the program dealt with theorem proving inside one formal system.

A note added to the proposal in 1996 records that there was no report from the summer project ^[2]. The proposal, and the accounts of what was shown at the meeting, remain the fixed points of the story; the coolness of the room when Logic Theorist was presented is part of the record as well ^[1].