Empirical Explorations with the Logic Theory Machine: A Case Study in Heuristics

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).