Division of Informatics

Forrest Hill & 80 South Bridge

## Research Paper #924 | |
---|---|

Title: | Verification of Diagrammatic Proofs |

Authors: | Jamnik,M; Bundy,A; Green,I |

Date: | Aug 1998 |

Presented: | Presented at Thinking with Diagrams Workshop, 1998 and AAAI Fall Symposium on Formalising Reasoning with Visual and Diagrammatic Representations (FRVDR) |

Keywords: | |

Abstract: | Human mathematicians often "prove" theorems by the use of diagrams and manipulations on them. We call these diagrammatic proofs. In Jamnik et al (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 schmatic proof. We 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. |

Download: | POSTSCRIPT COPY |