Proceedings of the Annual Meeting of the Cognitive Science Society

As models of human cognition, previous geometry theorem-proving programs were inappropriately influenced by the ease with which computers manipulate syntactic formulae. The failure of those programs to pay attention to h u m a n perception d o o m e d them as models of h o w humans solve geometry proof problems. Just as the study of theorem-proving once evolved into the study of planning, it is time n o w for theorem- proving to incorporate current ideas in the planning community. A close examination of what h u m a n s do w h e n they try to solve geometry proof problems, and of h o w geometry is taught, reveals an emphasis on chunks of problem-solving knowledge derived from examples, retrieved on the basis of visual cues. These ideas are characteristic of the case-based reasoning and situated activity approaches in planning. This paper concludes with a brief description and trace of a computer program, POLYA , which does reactive, memory-based geometry theorem-proving.