Mathematical Reasoning with Diagrams

From Intuition to Automation

by Mateja Jamnik

---

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 omega-rule. 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 meta-theory 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 self-contained, 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):297-321. 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. 23--30. 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. 528--533. 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. 168--175. 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 nineteen-fifties 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 mid-nineteen-thirties.

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 non-human 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 problem-solving 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, ..., 2n-1 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² 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
  • Barker-Plummer 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 omega-Rule and Schematic Proofs
  • Motivation
  • Constructive omega-Rule
  • Schematic Proof
  • Finding a Schematic Proof
  • Why Use Schematic Proofs?
  • Penrose, Goedel Argument and Constructive omega-Rule
  • 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 Example-Proofs
  • 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
  • Example-Proof Traces
  • Formalization of Schematic Proofs
  • Abstraction Techniques
  • Abstracting for All Linear Functions
  • Breaking c-Homogeneous to f-Homogeneous 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 omega-Rule
  • Logicians' Motivation for Using omega-rule
  • Example of Using the omega-rule
• 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 on Mateja dot Jamnik at cl dot cam dot ac dot uk.