This program is an interactive geometry software with proof related features.
The project consist in producing an interactive proof software for geometry.
GeoProof can communicate with the Coq proof assistant to perform automatic and interactive proofs of geometry theorems.
S. Wilson, and J. Fleuriot. Proceedings of the European Joint Conferences on Theory and Practice
of Software (ETAPS) Satellite Workshop on User Interfaces for Theorem
Provers (UITP), Edinburgh, UK, (April 2005)