Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Logic and Semantics Seminar
Monday 13th October, 1997: Mateja Jamnik
Computer Laboratory > Research > TSG > Logic and Semantics Seminar > Monday 13th October, 1997: Mateja Jamnik

Speaker: Mateja Jamnik, University of Edinburgh
Title: Automation of Diagrammatic Reasoning
Time: Monday 13th October, 1997, 14:00
Abstract:

(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.