- Abstract:
-
This paper outlines Geometry Explorer, a prototype system that allows users to create Euclidean geometry constructions using a dynamic geometry interface, specify conjectures about them and then use a full-angle method prover to automatically produce diagram independent, human-readable proofs to theorems. Our system can then automatically generate novel diagrammatic proofs of the forward-chaining and backward-chaining reasoning used by the geometry theorem prover, as well as visualise multiple proofs to single theorems. We discuss the features of our system, how they were implemented and the issues encountered when trying to create diagrammatic full-angle method proofs.
- Copyright:
- 2005 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @InProceedings{EDI-INF-RR-0242,
- author = {
Sean Wilson
and Jacques Fleuriot
},
- title = {Geometry Explorer: Combining Dynamic Geometry, Automated Geometry Theorem Proving and Diagrammatic Proofs},
- book title = {Proceedings of UITP 2005 (User Interfaces for Theorem Provers)},
- year = 2005,
- month = {Apr},
- }
|
