 |
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.