Informatics Report Series


Report   

EDI-INF-RR-0242


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Geometry Explorer: Combining Dynamic Geometry, Automated Geometry Theorem Proving and Diagrammatic Proofs
Authors: Sean Wilson ; Jacques Fleuriot
Date:Apr 2005
Publication Title:Proceedings of UITP 2005 (User Interfaces for Theorem Provers)
Publication Type:Conference Paper
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},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh