Mathematical Reasoning with Diagrams:
From Intuition to Automation
by Mateja Jamnik
Published by CSLI
Press, Stanford University, Stanford, CA
Distributed by Chicago
University Press
December, 2001, 204 pages
Hardback: ISBN 1575863235, £41.00 / $65.00.
Paperback: ISBN 1575863243, £15.50 / $24.00.
Buy my book form here: (CSLI PRESS, Amazon)
Abstract
Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems which humans can prove by the use of geometric operations on diagrams, so called diagrammatic proofs. This book investigates and describes how such diagrammatic reasoning about mathematical theorems can be automated.
Concrete, rather than general diagrams are used to prove particular instances of a universal statement. The "inference steps" of a diagrammatic proof are formulated in terms of geometric operations on the diagram. A general schematic proof of the universal statement is induced from these proof instances by means of the constructive omegarule. Schematic proofs are represented as recursive programs which, given a particular diagram, return the proof for that diagram. It is necessary to reason about this recursive program to show that it outputs a correct proof. One method of confirming that the abstraction of the schematic proof from the proof instances is sound is proving the correctness of schematic proofs in the metatheory of diagrams. The book presents an investigation of these ideas and their implementation in the system, called Diamond.
Preface
This book started as my doctoral dissertation (Jamnik 1999) under the supervision of Alan Bundy and Ian Green at the University of Edinburgh, in what was then known as the Department of Artificial Intelligence, and had by the end of my PhD studies become the Division of Informatics.
This book is written for a mathematically minded audience. The intention is to present an exploration into the subset of the world of mathematics which can be solved with the use of pictures. Some familiarity with logic is required to understand the entire contents of the book. However, readers with little or no knowledge of logic should be able to safely omit parts of three particularly technical chapters: most of Chapter 8 and Appendix B, and parts of Chapter 4. Chapter 8 and Appendix B, in particular, are not essential to understand the general line of argument taken in the book. The specialist audience that the book is intended to attract is the automated reasoning community. The general audience that it is intended to attract is a community of scientists in artificial intelligence, computer scientists, mathematicians, philosophers, psychologists, cognitive scientists, teachers of mathematics and anybody interested in mathematical recreations.
I have attempted to make this book selfcontained, and have included a comprehensive survey of other related work (see Chapter 2). In order to explain any possibly unfamiliar or unconventional use of terminology, I have included a Glossary of such terms at the end of the book.
Parts of the work described in this book have appeared in press in the past, in particular in (Jamnik et al. 1999), (Jamnik et al. 1998), (Jamnik et al. 1997b) and (Jamnik et al. 1997a).

(Jamnik 1999): On Automating Diagrammatic Proofs of Arithmetic
Arguments. Unpublished PhD thesis. Division of Informatics,
University of Edinburgh. 1999.

(Jamnik et al. 1999): On Automating Diagrammatic Proofs of
Arithmetic Arguments. (with A. Bundy and I. Green). Journal of Logic,
Language and Information. 8(3):297321. 1999. Also available as
Department of Artificial Intelligence Research Paper No. 910.

(Jamnik et al. 1998): Verification of Diagrammatic
Proofs. (with A. Bundy and I. Green). In Meyer, B., (ed.),
Proceedings of the 1998 AAAI Fall Symposium on Formalising Reasoning
with Visual and Diagrammatic Representations, pp. 2330. American
Association for Artificial Intelligence, AAAI Press. 1998. Also
published in the Proceedings of ``Thinking With Diagrams 1998''
Workshop. Also available from Edinburgh as DAI Research Paper No. 924.

(Jamnik et al. 1997b): Automation of Diagrammatic
Reasoning. (with A. Bundy and I. Green). In Pollack, M.E., (ed.),
Proceedings of the 15th IJCAI, vol. 1, pp. 528533. International
Joint Conference on Artificial Intelligence, Morgan Kaufmann
Publishers. 1997. Also published in the ``Proceedings of the 1997
AAAI Fall Symposium''. Also available from Edinburgh as DAI Research
Paper No. 873.
 (Jamnik et al. 1997b): Automation of Diagrammatic Proofs in Mathematics. (with A. Bundy and I. Green). In Kokinov, B., (ed.), Perspectives on Cognitive Science, vol. 3, pp. 168175. New Bulgarian University. 1997. Also available from Edinburgh as DAI Research Paper No. 835.
Acknowledgments
First and foremost, I would like to thank Alan Bundy for his invaluable advice, guidance and encouragement in my research. He has been an inspiration for me during these years.
I am indebted to Alan Robinson for not only being the first person to encourage me to publish this work as a book, but also for writing the foreword and giving me useful comments on a draft.
I would also like to thank Ian Green, Predrag Janicic, Nigel Shadbolt, Aaron Sloman and Keith Stenning for many useful discussions and comments on my work. Thanks to Manfred Kerber, Bob Lindsay and Toby Walsh for their comments on a draft of this book.
I especially thank Gavin Bierman for his love, understanding and encouragement throughout this time.
Lastly, to my family: najlepsa hvala moji druzini za
njihovo stalno ljubezen in podporo.
This work was supported by a studentship from the Department of Artificial Intelligence at the University of Edinburgh, by a supplementary grant from the Slovenian Scientific Foundation, by a studentship from the British Overseas Research Scheme, and by EPSRC grant GR/M22031.
Foreword by Prof. Alan Robinson
The advent of the modern computer in the nineteenfifties immediately suggested a new research challenge: to seek ways of programming these versatile machines which would make them behave as much like intelligent human beings as possible. After fifty years or so, this quest has produced some intriguing results, but until now progress has been disappointingly slow. This book is a welcome and encouraging sign that things may at last be about to change.
To be sure, what might be called the purely logical approach has recently produced some noteworthy successes. Consider the following two examples:
On October 10, 1996, a rigorous proof of the Robbins Conjecture was found by William McCune's theorem proving program EQP at the Argonne National Laboratory. This problem had been unsolved since the midnineteenthirties.
On May 11, 1997, the (then) world chess champion Garry Kasparov lost a six game match against the computer program Deep Blue with a score of 2.5 to 3.5: two wins for Deep Blue, one win for Kasparov and three draws.
Both these programs, however, use quite nonhuman methods. Neither of them is at all based on how the mind of the human expert actually works. It is in fact very difficult to find out what the natural intellectual processes of expert humans really are. To program a computer to solve the kind of problems that such experts can solve, the purely logical approach has hitherto been found more effective than the heuristic approach: to invent systematic algorithms for solving the problems rather than trying to discover, and then to imitate, the relevant human skills. Not that the heuristic approach has been ignored. On the contrary, heuristic problemsolving and the programming of ``expert system'' have been prominent computational methodologies in Artificial Intelligence and Operations Research from the beginning. But in mathematical theorem proving, at least, the purely logical approach has far outpaced the heuristic approach.
The fact is that the latter has been severely hampered by a shortage of insights into mathematical cognition and ratiocination. Professor Alan Bundy's group at the University of Edinburgh has for some time now been patiently and insightfully seeking to remedy this shortage. Mateja Jamnik developed the ideas described in this book as a member of Bundy's group, and the book beautifully illustrates what the group has been doing.
What is novel about Mateja Jamnik's work is that she has found an explanation of at least part of the mystery of how humans are able to ``see'' the truth of certain mathematical propositions merely by contemplating appropriate diagrams and constructions. This ability to ``see'' is one of the really fundamental components of the human mathematical cognitive repertoire. As the late great mathematician G. H. Hardy put it: in the last analysis there is no such thing as ``proof''  all a mathematician really does is observe what is there. To convince others of what he observes to be the case all he can do is point and say: do you see? Mateja Jamnik's program ``sees'', for example, as we do, that a 5 by 5 array of dots is also a nest of 5 ``ells'' containing respectively 1, 3, 5, 7, and 9 dots, and that there is nothing special about this special case. It and we can see that the case of 5 is but one instance of the general pattern whereby, for any n, an n by n array of dots is also a nest of n ``ells'' containing respectively 1, 3, 5, 7, ..., 2n1 dots. In this way it and we can directly see, as a kind of mathematical sense datum, the truth of the mathematical theorem that the number n^{2} is the sum of the first n odd numbers. This act of seeing is analyzed in the program as a set of alternative decompositions of a given square array; we can see it either as a row of columns: or as a column of rows, or as a nest of frames, or as a nest of ells, or as an array of subsquares, and so on and on. Each of these perceptions is the same as seeing the truth of a corresponding mathematical theorem.
It is as though the program Deep Blue had been given some of the very same abilities to ``see'' the right chess move as Kasparov  literally to see what he sees when he looks at the board. But we don't know what it is that Kasparov sees.
Impressive though some of its achievements have been (such as that of EQP mentioned above), the purely logical approach to mathematical theorem proving is limited in scope and scientifically unedifying. The present book is an encouraging demonstration that its scope can be much widened, and its explanatory power expanded, by a fearless and patient exploration of the details of actual mathematical cognition. The logical and the heuristic approaches are beginning to come together in a most fruitful way. Mateja Jamnik is among the pioneers of a fresh new approach to an old problem.
I welcome the elegant and surprising insights of this book as ushering in a new generation of discoveries in the understanding of mathematical reasoning.
J.A.Robinson
Professor Emeritus, Syracuse University
May, 2001
Table of Contents
 Foreword
 Preface
 1: Introduction
 Motivation
 Aims
 Some Original Contributions
 Layout of the Rest of This Book
 2: The History of Diagrammatic Systems
 Gelernter's Geometry Machine
 Koedinger and Anderson's DC
 BarkerPlummer and Bailin's ``&''/Grover
 Barwise and Etchemendy's Hyperproof
 Lindsay's Archimedes
 Furnas' Bitpict
 Anderson and McCartney's IDR
 Logic of Diagrams
 Other Related Systems
 Summary
 3: Diagrammatic Theorems and the Problem Domain
 Diagrams and Proofs
 `Diagrammatic' Theorems
 Classification
 Abstraction Devices for Representation of Diagrams
 Problem Domain
 Summary
 4: The Constructive omegaRule and Schematic Proofs
 Motivation
 Constructive omegaRule
 Schematic Proof
 Finding a Schematic Proof
 Why Use Schematic Proofs?
 Penrose, Goedel Argument and Constructive omegaRule
 Diagrams and Schematic Proofs
 Schematic Diagrammatic Proofs for Theorems of Category 2
 Summary
 5: Designing a Diagrammatic Reasoning System
 Overview of Diamond
 Architecture
 Diamond's Notion of Proof
 Construction of ExampleProofs
 Representations
 Interface
 Summary
 6: Diagrammatic Operations
 Choice of Operations
 Multiple Representations of Diagrams
 Operations and Representations of Diagrams
 Operations as Tactics
 Diagram Representation and Induction Schema
 Summary
 7: The Construction of Schematic Proofs
 Context for Abstraction
 ExampleProof Traces
 Formalization of Schematic Proofs
 Abstraction Techniques
 Abstracting for All Linear Functions
 Breaking cHomogeneous to fHomogeneous Proof
 Proofs With Case Splits
 Abstracting From One Example
 Summary
 8: The Verification of Schematic Proofs
 Motivation
 Diagrams
 Operators
 Operations
 Function definitions
 Correctness of Schematic Proofs
 Size of Diagrams
 Algebraic Correctness of Schematic Proofs
 Arithmetic Conjecture and Diagrammatic Proof
 Implementation of Theory of Diagrams
 Summary
 9: Diamond in Action
 Example of Diamond's Diagrammatic Proof
 Evaluation Issues
 Summary
 10: Complete Automation
 Complete Automation of a Diagrammatic Theorem Prover
 The Context of Our Work
 Have We Achieved the Aims?
 A: More Examples of Diagrammatic Theorems
 Pythagoras' Theorem II
 Triangular Equality for Odd Squares
 Even Triangular Sum
 Sum of All Natural Numbers
 Euler's Theorem
 B: The omegaRule
 Logicians' Motivation for Using omegarule
 Example of Using the omegarule
 Glossary
 Bibliography
 Index
Bibliography
The pdf of the bibliography is here.
Errata
I would be greatful if you report any errors that you may find in the book to me by email.