Automation of Diagrammatic Reasoning

Theoremsin automated theorem proving are usually proved by logical formal proofs. However,there is a subset of problems which humanscan prove in a different wayby the use of geometric operations on diagrams, so called diagrammaticproofs. Insight is moreclearly perceived in these than in the correspondingalgebraic proofs: they capture an intuitive notion of truthfulness that humansfind easy to see and understand. Weare identifying and automating this diagrammaticreasoning on mathematical theorems. The user gives the system, called DIAMOND,a theoremand then interactively provesit by the use of geometric manipulations on the diagram. Theseoperations are the "inference steps" of the proof. DIAMONDthen automatically derives from these example proofs a generaJisedproof. Theconstructive w-rule is used as a mathematicalbasis to capture the generality of inductive diagrammaticproofs. In this way,we explore the relation betweendiagrammaticand algebraic proofs.

• Type: Conference
• Year: 1997
• Where: IJCAI
• Authors: Mateja Jamnik, Alan Bundy, Ian Green
• Keywords: Automated Theorem Proving, Correspondingalgebraic Proofs, IJCAI 1997, IJCAI 2007, Logical Formal Proofs