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.