Logic Theorist

Logic Theorist is a computer program written in 1955 and 1956 by Allen Newell, Herbert A. Simon and Cliff Shaw. It was the first program deliberately engineered to mimic the problem solving skills of a human being and is called "the first artificial intelligence program". It would eventually prove 38 of the first 52 theorems in Whitehead and Russell's Principia Mathematica, and find new and more elegant proofs for some.

In 1955, when Newell and Simon began to work on the Logic Theorist, the field of artificial intelligence did not yet exist. Even the term itself ("artificial intelligence") would not be coined until the following summer.

Simon was a political scientist who had already produced classic work in the study of how bureaucracies function as well as developed his theory of bounded rationality (for which he would later win a Nobel Prize). The study of business organizations may seem, on the surface, to be very different from artificial intelligence, but it requires the same insight into the nature of human problem solving and decision making. Simon remembers consulting at RAND in the early 1950s and seeing a printer typing out a map, using ordinary letters and punctuation as symbols. He realized that a machine that could manipulate symbols could just as well simulate decision making and possibly even the process of human thought.

The program that printed the map had been written by Newell, a RAND Corporation scientist studying logistics and organization theory. For Newell, the decisive moment was in 1954 when Oliver Selfridge came to RAND to describe his work on pattern 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. It was a rare moment of scientific epiphany.

...
Wikipedia