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.