TY - GEN
T1 - Automation of Diagrammatic Reasoning
AU - Jamnik, Mateja
AU - Bundy, Alan
AU - Green, Ian
PY - 1997
Y1 - 1997
N2 - 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.
AB - 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.
M3 - Conference contribution
SN - 1558604804
BT - Proceedings of the 15th International Joint Conference on Arti Intelligence - IJCAI '97
PB - Morgan Kaufmann
ER -