This paper describes POLYA, a computer program that writes geometry proofs. POLYA actively collects features from a geometry diagram on the basis of which it recognizes and applies knowledge from known examples. We present a vocabulary of visual targets, results, and actions to support incremental parsing of diagrams. W e also show how scripts can be used to organize visual actions into useful sequences. W e show how those sequences can be used to parse diagrams and instantiate proofs. Finally, we show how scripts represent the implicit spatial knowledge conveyed by examples.
