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.

Mateja Jamnik is a research fellow in the School of Computer Science at The University of Birmingham in the United Kingdom.

Read an excerpt from this book.

- Foreword vii
- Preface xi
- 1 Introduction 1
- 2 The History of Diagrammatic Systems 11
- 3 Diagrammatic Theorems and the Problem Domain 27
- 4 The Constructive !-Rule and Schematic Proofs 49
- 5 Designing a Diagrammatic Reasoning System 71
- 6 Diagrammatic Operations 89
- 7 The Construction of Schematic Proofs 103
- 8 The Verification of Schematic Proofs 123
- 9 Diamond in Action 149
- 10 Complete Automation 163
- Appendix A: More Examples of Diagrammatic Theorems 175
- Appendix B: The w-Rule 181
- Glossary 185
- References 190
- Index 199

11/30/2001