Diamond: Diagrammatic Reasoning System Demonstration

Mateja Jamnik, Alan Bundy, Ian Green

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.