Proceedings of the Annual Meeting of the Cognitive Science Society

This paper analyzes how mathematicians prove theorems. The analysis is based upon several empirical sources such as reports of mathematicians and mathematical proofs by analogy In order to combine the strength of Uaditional automated theorem provers with human-like capabilities, the questions arise: Which problem solving strategies are appropriate? Which representations have to be employed? As a result of our analysis, the following reasoning su^tegies are recognized: proof planning with partially instantiated methods, structuring of proofs, the transfer of subproofs and of reformulated subproofs. W e discuss the representation of a component of these reasoning suategies, as well as its properties. W e find some mechanisms needed for theorem proving by analogy, that are not provided by previous approaches to analogy. This leads us to a computational representation of new components and procedures for automated theorem proving systems.