GeoView is a tool that combines the Coq theorem prover with the dynamic geometry drawing tool GeoplanJ developed at CNAM. GeoView is an extension of the user-interface Pcoq and is dedicated to the visualization of formal statements of plane geometrical theorems. The statements of geometrical theorems and their proofs are constructed and verified with Coq theorem prover. A dynamic figure is automatically associated to mathematical formulas to show the meaning of these statements. The figures generated with GeoView can be integrated as interactive and dynamic figures in HTML files using the GeoplanJ applet.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element