DIAMOND: Diagrammatic Reasoning System Demonstration*
J Mateja, Alan Bundy, Ian Green · 1998
We demonstrate an interactive diagrammatic reasoning system DI AMOND, which proves theor ems of natural number arithmetic. The user co n structs concrete proofs of ground instances of a theorem by applying geometric operations to a diagram. DIAMOND then automatically derives from these example proofs a generalised proof, called a schematic proof, and checks that this is indeed a proof of the theorem. DIAMOND (Diagrammatic Reasoning and Deduction) is a diagrammatic proof system implemented in the functional programming language Standard NIL of :\few Jersey version 109. For detailed information on DIA MOND, the reader is referred to (Jamnik, Bundy, & Green 1997) and our paper entitled Verificat'of dia grammatic proofs published in this volume. In DIAMOND we exploit the property that diagrams can be drawn for concrete instances of theorems. In stead of using abstractions to express general diagrams, DIAMOND captures the generality of the diagrammatic proof with a recursive program which when instantiated for each value of a parameter generates a proof for the corresponding instance of a theorem. The extraction of the recursive program consists of three steps: • the interactive construction of example proofs, • the automatic extraction of a schematic proof, • the automatic verification of this schematic proof. Ground Instances of a Diagrammatic Proof An example proof is constructed interactively with the user It consists of a sequence of geometric operations that need to be applied to the diagram. The geometric operations capture the inference steps of the proof. This sequence in some way justifies, i. e. proves, some ground instance of the theorem. (Jamnik, Bundy, & Green 1997)