Robert K. Lindsay
This research is developing a computational model of the use of diagrams in the understanding of mathematical concepts. The model represents diagrams with a combination of pixel arrays and propositional descriptions. It applies a general simulation algorithm to the pixel representation to verify inferences, following the directions of a person attempting to demonstrate a theorem or conjecture of plane geometry. Such reasoning involves both spatial and verbal reasoning, and a major aspect of this research is to describe with computational precision how these modes interact. This paper addresses one important aspect of this problem, namely, how to represent general conclusions that are discovered by examination of a specific diagram. In other words, the question is how to represent quantification over classes of figures while retaining the use of inference by simulation that applies only to particular instances.