(work with Alan Bundy and Ian Green)
Mathematical Reasoning Group
Department of Artificial Intelligence
University of Edinburgh
Theorems in automated theorem proving are usually proved by formal
logical proofs. However, there is a subset of problems which humans
can prove by the use of geometric operations on diagrams, so called
diagrammatic proofs. Insight is often 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 investigating and automating such diagrammatic reasoning about
mathematical theorems. The user gives the system, called DIAMOND, a
theorem and then interactively proves particular concrete instances of
it by the use of geometric operations on the diagram. These operations
are the ``inference steps'' of the proof. DIAMOND then automatically
induces from these proof instances a generalised schematic proof. The
constructive omega-rule is used as a mathematical basis for such
generalised schematic proofs. This approach allows us to embed the
generality in the schematic proof so that operations need only be
applied to concrete diagrams. We are investigating the translation of
such schematic proofs into algebraic proofs as one route to confirm
that the generalisation of the schematic proof from the proof
instances is sound.
|