Division of Informatics

Forrest Hill & 80 South Bridge

## Research Paper #835 | |
---|---|

Title: | Automation of Diagrammatic Proofs in Mathematics |

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

Date: | Dec 1996 |

Presented: | Presented at The Third International Summer School in Cognitive Science, Sofia, Bulgaria, 1996 - Proceedings : Perspectives on Cognitive Science. |

Keywords: | |

Abstract: | Theorems in automated theorem proving are usually proved by logical formal proofs. However, there is a subset of problems which can also be proved in a more informal way by the use of geometric operations on diagrams, so called diagrammatic proofs. Insight is more clearly perceived in these than in the corresponding logical proofs: they capture an intuitive notion of truthfulness that humans find easy to see and understand. The proposed research project is to identify and ultimately automate this diagrammatic reasoning on mathematical theorems. The system that we are in the process of implementing will be given a theorem and will (initially) interactively prove it by the use of geometric manipulations on the diagram that the user chooses to be the appropriate ones. These operations will be the inference steps of the proof. The constructive $\omega $ rule will be used as a tool to capture the generality of diagrammatic proofs. In this way, we hope to verify and to show that the diagrammatic proof of a gven theorem can be formalised. |

Download: | POSTSCRIPT COPY |