This page in English

  GeoView

GeoView est un outil qui marie l'outil de construction de figures dynamiques interactives GeoplanJ developpé par le CNAM au système de preuve Coq.
Geoview est une extension de l'interface graphique Pcoq qui permet de visualiser les énoncés de théorèmes de géométrie plane.

Les énoncés des théorèmes et leurs preuves sont construits et vérifiés avec le système Coq.
Une figure dynamique est automatiquement associée aux formules mathématiques et donne une représentation graphique de l'énoncé formel.
Les figures générées par GeoView peuvent être intégrées comme figures dynamiques dans des pages HTML en utilisant l'applet GeoplanJ.

Voici un exemple d'un théorème sur la conservation de l'alignement par les homothéties (on trouvera d'autres exemples ici).

 

Ci-dessous la figure dynamique générée par GeoView :

On peut déplacer les points libres (en vert) en utilisant le bouton gauche de la souris.
En double-cliquant sur la figure, on obtient un menu qui permet de construire de nouveaux objets (points, droites ...)
Le nombre réel k est représenté par un point sur une droite. On peut changer sa valeur en déplaçant ce point.

 

 

GeoView est écrit en Java et a été intégré à Pcoq construit et maintenu par l'équipe Lemme à l'INRIA Sophia-Antipolis.

Dernière mise à jour de cette page