On the practical semantics of mathematical diagrams. This chapter describes the authors’ research into the way in which diagrams convey mathematical meaning. Through the development of an automated reasoning system, called &/GROVER, we have tried to discover how a diagram can convey the meaning of a proof. &/GROVER is a theorem-proving system that interprets diagrams as proof strategies. The diagrams are similar to those that a mathematician would draw informally when communicating the ideas of a proof. We have applied &/GROVER to obtain automatic proofs of three theorems that are beyond the reach of existing theorem-proving systems operating without such guidance. In the process, we have discovered some patterns in the way diagrams are used to convey mathematical reasoning strategies. Those patterns, and the ways in which &/GROVER takes advantage of them to prove theorems, are the focus of this chapter.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element