 For instance, Harel  (1988)  invented higraphs to represent system specifications in computer science. This idea has been taken up in industrial applications (e.g., UML, in Booch et al.  1998).  Barker-Plummer &amp; Bailin  (1997)  present a case study in developing computers which can carry out the kind of analogical reasoning that humans perform when proving certain mathematical theorems. More recently, an interesting result has been presented by Mateja Jamnik of Alan Bundy’s Mathematical Reasoning Group at Edinburgh (Jamnik  2001).  Jamnik shows how a semi-automatic formal proof system can perform some of the perceptual inferences which humans find so natural. For instance, that the sum of the first n odd natural numbers is n squared is easily seen by decomposing an n × n grid into “ells” (Jamnik et al.  1999).