Mathematical reasoning with diagrams : from intuition to automation
Mateja Jamnik · 2001
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.