On Automated Scientific Theory Formation: A Case Study using the AM Program

A program called "AM" is described which carries on simple mathematics research, defining and studying new concepts under the guidance of a large body of heuristic rules, but does not synthesize new heuristics for dealing effectively with those new concepts.

Abstract

A program called is described which carries on simple mathematics research, defining and studying new concepts under the guidance of a large body of heuristic rules. The 250 heuristics communicate via an agenda mechanism, a global priority queue of small tasks for the program to perform, and reasons why each task is plausible (for example, Find generalizations of 'primes', because 'primes' turned out to be so useful a concept). Each concept is represented as an active, structured knowledge module. One hundred very incomplete modules are initially supplied, each one corresponding to an elementary set-theoretic concept (for example, union). This provides a definite but immense space which AM begins to explore. In one hour, AM rediscovers hundreds of common concepts (including singleton sets, natural numbers, arithmetic) and theorems (for example, unique factorization). As AM defines concepts, and fills in their facets, it does not synthesize new heuristics for dealing effectively with those new concepts. This inability turns out to be its main limitation.