Graduate studies at Western
Journal of Logic, Language and Information 8 (3):297-321 (1999)
|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.|
|Keywords||automated reasoning diagrammatic reasoning theorem proving|
|Categories||categorize this paper)|
|Through your library||Configure|
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.
Carlo Cellucci (2008). Why Proof? What is a Proof? In Giovanna Corsi & Rossella Lupacchini (eds.), Deduction, Computation, Experiment. Exploring the Effectiveness of Proof, pp. 1-27. Springer.
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 downloads4 ( #189,403 of 739,125 )
Recent downloads (6 months)1 ( #61,778 of 739,125 )
How can I increase my downloads?