GeoProof svn2006-08-24

GeoProof project is a dynamic geometry application with proof related features.
GeoProof project is a dynamic geometry application with proof related features.

It can communicate with the Coq proof assistant to perform automatic and interactive proofs of theorems.

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.

GeoProof is developed mainly by Julien Narboux from a project called DrGeoCaml initiated by Nicolas François.

Main features:

  • computations are done using arbitrary precision thanks to the creal library by Jean-Christophe Filliâtre.
  • some theorems can be checked using the automated theorem proving methods implemented by John Harrison.
  • GeoProof can communicate with CoqIde (a user interface for Coq). The user can build a construction using GeoProof and the corresponding formula is automatically translated into Coq's syntax.

last updated on:
November 1st, 2006, 14:05 GMT
price:
FREE!
developed by:
Billy
license type:
GPL (GNU General Public License) 
category:
ROOT \ Education

FREE!

In a hurry? Add it to your Download Basket!

user rating

UNRATED
0.0/5
 

0/5

Add your review!

SUBMIT