Edinburgh Research Explorer

Automation of Diagrammatic Reasoning

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

Related Edinburgh Organisations

Open Access permissions

Open

Documents

http://hdl.handle.net/1842/4548
Original languageEnglish
Title of host publicationProceedings of the 15th International Joint Conference on Arti Intelligence - IJCAI '97
PublisherMorgan Kaufmann
ISBN (Print)1558604804
StatePublished - 1997

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.

Download statistics

No data available

ID: 403132