A Model of Interaction with Geometry Diagrams

Reasoning with Diagrammatic Representations

Volume

Reasoning with Diagrammatic Representations

Contents

This paper describes POLYA, a model of diagram use in support of geometry theorem-proving. POLYA collects features from the diagram via a shifting focus of attention. It uses those features to index search scripts---routines to look for significant patterns in the diagram---and proof scripts--routines for translating objects in the diagram into statements in the proof. This paper presents a partial vocabulary of visual focus and action, suggests some scripts for recognizing useful patterns, and describes a mechanism for script selection.