In Proving Theorems as Done by Man, Logician, or Machine, pp. 215-233. Proc. Summer Institute for Symbolic Logic

In Applications of Logic to Advanced Digital Computer Programming, Ann Arbor, Mich: University of Michigan Press

IRE Convention Record, pp. 56-62 (

This is a case study in problem-solving, representing part of a program of research on complex information-processing systems. We have specifieda system for finding proofs of theorems in elementary symbolic logic, and by programming a computer to these specifications, have obtained empirical data on the problem-solving process in elementary logic. The program is called the Logic Theory Machine (LT); it was devised to learn how it is possible to solve difficult problems such as proving mathematical theorems, discovering scientific laws from data, playing chess, or understanding the meaning of English prose.The research reported here is aimed at understanding the complexp rocesses (heuristics) that are effective in problem-solving. Hence, we are not interested in methods that guarantee solutions, but which require vastamounts of computation. Rather, we wish to understand how a mathematician, for example, is able to prove a theorem even though he does not know when he starts how, or if, he is going to succeed.Proceedings of the Western Joint Computer Conference, 15:218-239. Reprinted in Feigenbaum and Feldman, Computers and Thought (1963).

The recent work of the Unit has been primarily concerned with the employment ofthesauri in machine translation. Limited success has been achieved, in punchedcardtests, in improving the idiomatic quality and so the intelligibility of an initiallyunsatisfactory translation, by word-for-word procedures, from Italian intoEnglish, by using a program which permitted selection of final equivalents from"heads" in Roget's Thesaurus, i.e. lists of synonyms, near-synonyms and associatedwords and phrases, instead of from previously determined lists of alternativetranslations. Mechanical Translation, vol.4, nos.1 and 2, November 1957; pp. 35-43]

In Proving Theorems as Done by Man, Logician, or Machine, pp. 215-233. Proc. Summer Institute for Symbolic Logic

Artificial Intelligence Project, Dartmouth College, Hanover, Vt, August, mimeographed

John Wiley & Sons, New York

Proc. First Intern. Congress of Cybernetics, Namur, 8S-56

Between 1946 and 1956, a number of BBC radio broadcasts were made by pioneers in the fields of computing, artificial intelligence and cybernetics. Although no sound recordings of the broadcasts survive, transcripts are held at the BBC's Written Archives Centre at Caversham in the UK. This paper is based on a study of these transcripts, which have received little attention from historians. The paper surveys the range of computer-related broadcasts during 1946-1956 and discusses some recurring themes from the broadcasts, especially the relationship of'artificial intelligence' to human intelligence.