The University of Edinburgh -
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.
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.

[Search These Pages] [DAI Home Page] [Comment]