Verification of Diagrammatic Proofs

Contents

Human mathematicians often "prove" theorems by the use of diagrams and manipulations on them. We call these diagrammatic proofs. In (Jamnik, Bundy, and Green 1997) we presented how "informal" reasoning with diagrams can be automated. Three stages of proof extraction procedure were identified. First, concrete rather than general diagrams are used to prove particular instances of the universally quantified theorem. The diagrammatic proof is captured by the use of geometric operations on the diagram. Second, an abstracted schematic proof of the universally quantified theorem is automatically induced from these proof instances. Third, the final step is to confirm that the abstraction of the schematic proof from the proof instances is sound. Our main focus in this paper is on the third stage, the verification of schematic proofs. We define a theory of diagrams where we prove the correctness of a schematic proof. Vie give an example of an extraction of a schematic proof for a theorem about the sum of odd naturals, and prove its correctness in the theory of diagrams.