David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
Journal of Logic, Language and Information 8 (3):297-321 (1999)
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)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
Matej Urbas, Mateja Jamnik & Gem Stapleton (2015). Speedith: A Reasoner for Spider Diagrams. Journal of Logic, Language and Information 24 (4):487-540.
Similar books and articles
John Mumma (2012). Constructive Geometrical Reasoning and Diagrams. Synthese 186 (1):103-119.
Jan Krajíček (2004). Implicit Proofs. Journal of Symbolic Logic 69 (2):387 - 397.
John W. Dawson Jr (2006). Why Do Mathematicians Re-Prove Theorems? Philosophia Mathematica 14 (3):269-286.
N. Shankar (1994). Metamathematics, Machines, and Gödel's Proof. Cambridge University Press.
John Mumma (2010). Proofs, Pictures, and Euclid. Synthese 175 (2):255 - 287.
Brice Halimi (2012). Diagrams as Sketches. Synthese 186 (1):387-409.
Jeremy Avigad (2006). Mathematical Method and Proof. Synthese 153 (1):105 - 159.
Sun-Joo Shin (2012). The Forgotten Individual: Diagrammatic Reasoning in Mathematics. Synthese 186 (1):149-168.
David Sherry (2009). The Role of Diagrams in Mathematical Arguments. Foundations of Science 14 (1-2):59-74.
Added to index2009-01-28
Total downloads9 ( #291,670 of 1,780,278 )
Recent downloads (6 months)1 ( #291,765 of 1,780,278 )
How can I increase my downloads?