Automation of Diagrammatic Reasoning

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 w-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.