Diamond: Diagrammatic Reasoning System Demonstration

Contents

We demonstrate an interactive diagrammatic reasoning system DIAMOND, which proves theorems of natural number arithmetic. The user constructs 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.