Mathematical Reasoning With Diagrams. From Intuition To Automation

Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems that 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 w-rule. Schematic proofs are represented as recursive programs, which when given a particular diagram return a 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 the soundness of the abstraction of a schematic proof from proof instances is to prove the correctness of the schematic proof in the meta-theory of diagrams. This book presents an investigation of these ideas and their implementation in a system called DIAMOND.