On automating diagrammatic proofs of arithmetic arguments

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. Insight is often more clearly perceived in these proofs than in the corresponding algebraic proofs; they capture an intuitive notion of truthfulness that humans find easy to see and understand. We are investigating and automating such diagrammatic reasoning about mathematical theorems. Concrete, rather than general diagrams are used to prove particular concrete instances of the universally quantified theorem. The diagrammatic proof is captured by the use of geometric operations on the diagram. These operations are the inference steps of the proof. An abstracted schematic proof of the universally quantified theorem is induced from these proof instances. The constructive -rule provides the mathematical basis for this step from schematic proofs to theoremhood. In this way we avoid the difficulty of treating a general case in a diagram. 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. These ideas have been implemented in the system, called Diamond, which is presented here.
Keywords automated reasoning  diagrammatic reasoning  theorem proving
Categories (categorize this paper)
Reprint years 2004
DOI 10.1023/A:1008323427489
 Save to my reading list
Follow the author(s)
Edit this record
My bibliography
Export citation
Find it on Scholar
Mark as duplicate
Request removal from index
Revision history
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 30,765
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA
Speedith: A Reasoner for Spider Diagrams.Matej Urbas, Mateja Jamnik & Gem Stapleton - 2015 - Journal of Logic, Language and Information 24 (4):487-540.

Add more citations

Similar books and articles
Implicit Proofs.Jan Krajíček - 2004 - Journal of Symbolic Logic 69 (2):387 - 397.
Why Do Mathematicians Re-Prove Theorems?John W. Dawson Jr - 2006 - Philosophia Mathematica 14 (3):269-286.
Proofs, Pictures, and Euclid.John Mumma - 2010 - Synthese 175 (2):255 - 287.
Diagrams as Sketches.Brice Halimi - 2012 - Synthese 186 (1):387-409.
.[author unknown] - unknown
The Role of Diagrams in Mathematical Arguments.David Sherry - 2009 - Foundations of Science 14 (1-2):59-74.
Added to PP index

Total downloads
14 ( #369,857 of 2,214,489 )

Recent downloads (6 months)
2 ( #238,730 of 2,214,489 )

How can I increase my downloads?

Monthly downloads
My notes
Sign in to use this feature