The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #873

Title:Automation of Diagrammatic Reasoning
Authors:Jamnik,M; Bundy,A; Green,I
Date:Oct 1997
Presented:To be presented at IJCAI-97 - AAAI-Fall Symposium working notes
Abstract:Theorems in automated theorem proving are usually proved by logical formal proofs. However, there is a subset of problems which humans can prove in a different way by the use of geometric operations on diagrams, so called diagrammatic proofs. Insight is more clearly perceived in these than in the corresponding algebraic proofs: they capture an intuitive notion of truthfulness that humans find easy to see and understand. We are identifying and automating this diagrammatic reasoning on mathematical theorems. the user gives the system, called DIAMOND, a theorem and then interactively proves it by the use of geometric manipulations on the diagram. These operations are the "inference steps" of the proof. DIAMOND then automatically derives from these example proofs a generalised proof. The constructive omega rule is used as a mathematical basis to capture the generality of inductive diagrammatic proofs. in this way, we explore the relation between diagrammatic and algebraic proofs.

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