A Model of Interaction with Geometry Diagrams

T. McDougal and K. Hammond

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.