Mathematical Reasoning With Diagrams: From Intuition to Automation

Mathematicians at every level use diagrams to prove theorems. *Mathematical Reasoning with Diagrams* investigates the possibilities of mechanizing this sort of diagrammatic reasoning in a formal computer proof system, even offering a semi-automatic formal proof system-called Diamond-which allows users to prove arithmetical theorems using diagrams.