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

Division of InformaticsForrest Hill & 80 South Bridge