On automating diagrammatic proofs of arithmetic arguments

Journal of Logic, Language and Information 8 (3):297-321 (1999)
  Copy   BIBTEX

Abstract

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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,164

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

.[author unknown] - unknown
Diagrams as sketches.Brice Halimi - 2012 - Synthese 186 (1):387-409.
Proofs, pictures, and Euclid.John Mumma - 2010 - Synthese 175 (2):255 - 287.
Metamathematics, machines, and Gödel's proof.N. Shankar - 1994 - New York: Cambridge University Press.
Why do mathematicians re-prove theorems?John W. Dawson Jr - 2006 - Philosophia Mathematica 14 (3):269-286.
Implicit Proofs.Jan Krajíček - 2004 - Journal of Symbolic Logic 69 (2):387 - 397.
The role of diagrams in mathematical arguments.David Sherry - 2008 - Foundations of Science 14 (1-2):59-74.

Analytics

Added to PP
2009-01-28

Downloads
39 (#386,963)

6 months
10 (#213,340)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Kant’s Crucial Contribution to Euler Diagrams.Jens Lemanski - 2024 - Journal for General Philosophy of Science / Zeitschrift für Allgemeine Wissenschaftstheorie 55 (1):59–78.
Diagrams.Sun-Joo Shin - 2008 - Stanford Encyclopedia of Philosophy.
Architecture-based conceptions of mind.Aaron Sloman - 2002 - In Peter Gardenfors, Katarzyna Kijania-Placek & Jan Wolenski (eds.), In the Scope of Logic, Methodology, and Philosophy of Science (Vol Ii). Kluwer Academic Publishers.
The well-designed young mathematician.Aaron Sloman - 2008 - Artificial Intelligence 172 (18):2015-2034.

View all 8 citations / Add more citations