Automated Theory Formation in Mathematics
Douglas B. Lenat · Contemporary mathematics - American Mathematical Society · 1984
A program called "AM " is described which cairies on simple mathematics research: defining, and studying new concepts under the guidance of a large body of heuiistic rules. The 250 heurKtus communicate via an agenda mechanism, a global priority queue of small bisk', for the program to pei foim and teasons why each task is plausible (e.g., "Find PENCRAHZTION. of 'prnes', because turued out to be so useful a Conccpi"). Fach concept is an active, structured knowledge module. One bundled vei y incomplete modules are initially supplied, each one corresponding to an elementary set theoretic concept (e.g., union). This provides a definite but immense space which AM begins to explore. In one boor, AM rediscovers hundreds of common concepts (including singleton sets, natural numbers, arithmetic) and theorems (e.g., unique factorization).