Proceedings of the Annual Meeting of the Cognitive Science Society

This paper presents the architecture of the discovery system SHUNYATA which models studies research in higher mathematics. SHUNYAT A analyzes mathematical proofs and product's concrpisand proof strategies which form the basis for the discovery of more difficult proofs in other mcichomatical theories. Its architecture avoids combinatorial explosions and does not, recijuire search str;uegies.The proof strategies contain two categories of predicates. A predicate of (he first caregoiy •^v-iirtsa small set of proof steps and the predicates of the second category evaluate partial proofs .uid decide which predicate of the first category should be apphed next. Thus, the proof strattgics includefeedback loops. A detailed example is given. It contains a simple proof in group theory, tlie .m-ilysisof this proof, and the discovery of a proof in lattice theory whose degree of diBiculty repremis r.hestate-of-the-art in automated theorem proving. The most important result of this work is tli".' discovery of a holistic logic based on the concept that cognitive structures arise from simple perceptions,evolve by reflection and finally contain their own evolution mechanisms.Keywords: Learning, knowledge acquisition, cognitive evolution, automated theorem proving.