Automation of Diagrammatic Reasoning

Mateja Jamnik, Alan Bundy, Ian Green

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationProceedings of the 15th International Joint Conference on Arti Intelligence - IJCAI '97
PublisherMorgan Kaufmann
ISBN (Print)1558604804
Publication statusPublished - 1997


Dive into the research topics of 'Automation of Diagrammatic Reasoning'. Together they form a unique fingerprint.

Cite this