USING DIAGRAMS TO UNDERSTAND GEOMETRY

This paper describes ARCHIMEDES-STUDENT, a computer program that constructs and modifies its own repre- sentations of diagrams from instructions supplied by a human who is demonstrating a theorem of geometry. The program's representation permits it to make inferences from its constructions and to find a justification for the conclusion of the theorem. It is argued that the sort of perceptual reasoning displayed by this program represents one important aspect of understanding because it relates the abstract mathematical theorem to knowledge of spa- tial relations. For humans this approach grounds abstraction in experience and thus provides a more compelling demonstration than a formal proof. Because ARCHIMEDES-STUDENT is a well-defined computer program, it provides a precise suggestion of how this aspect of understanding can be achieved. Theorems of plane geometry are generally illustrated in textbooks by diagrams. For most students a diagram facilitates following or discovering a proof. The diagram also appears to be valuable, perhaps essential, for literally and figuratively seeing the meaning of the theorem and understanding why it is interesting. Indeed formal proofs often add little to the understanding afforded by diagrams coupled with informal explanation, particularly for people not trained in mathematics. This paper is an exploration of the computational processes that underlie such use of diagrams as aids to understanding geometrical propositions. A proof in the modern, post-Hilbert sense is a sequence of statements in a precisely defined formal language composed of strings of characters from a finite alphabet. Each statement is justified by applying precise rules of deduction to preceding statements, such as axioms, previously proved lemmas, and theorems. Diagrams can have no essential place in this strict sense of theorem proving because they have no accepted syntax or semantic theory specified in the standard logical formalism. This is not an inherent limitation of diagrams and several recent efforts have attempted to fill this vacuum; see Barwise and Etchemendy (1990, 1992), Kaufman (1991), Shin (1991, 1992, 1995), Stenning and Oberlander (1992), Barker-Plummer and Bailin (1992), and Wang (1995), whose work is discussed further below. Although the several formal theories of diagrams that have been thus proposed are not fully general, it is fairly certain that no substantive obstacle stands in the way of further developments. Nonetheless, diagrams, even without a formal theory, clearly serve for humans a useful heuristic and pedagogical purpose that extends well beyond geometry textbooks, and includes the understanding of nongeometric mathematics, of physical principles, and even of informal biological and social theories. Diagrams and other graphical illustrations are ubiquitous conveyers of meaning and intuition even without a formal theory. There is much anecdotal evidence for this claim, as well as a number of systematic studies of the use of visual images in scientific discovery (e.g., Miller 1984; Thagard & Hardy 1992). In contrast to the formal proofs alluded to above, geometry is generally introduced to students by a combination of diagrams and quasi-formal "textbook proofs." Although text- book proofs lack the rigor of fully axiomatized formal proofs, they maintain the sentential, sequential proof structure while permitting more flexible use of natural language. Thus they