Premiers pas vers un cours de géométrie en Coq pour le lycée

Frédérique Guilhot 1
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Résumé : Nous présentons dans ce rapport une bibliothèque de géométrie en Coq dédiée-l'enseignement au lycée. L'accent est porté sur l'utilisation de l'interface graphique Pcoq et sur l'outil de construction GeoView qui permettent de présenter des énoncés et des figures proches de ceux utilisés au lycée. L'axiomatique choisie pour la formalisation n'utilise pas la méthode analytique. Nous présentons quelques exemples significatifs de preuves puis abordons les difficultés rencontrées dans ce travail.
Document type :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00071689
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 6:32:46 PM
Last modification on : Saturday, January 27, 2018 - 1:31:01 AM
Long-term archiving on: Sunday, April 4, 2010 - 10:33:26 PM

Identifiers

  • HAL Id : inria-00071689, version 1

Collections

Citation

Frédérique Guilhot. Premiers pas vers un cours de géométrie en Coq pour le lycée. RR-4893, INRIA. 2003. ⟨inria-00071689⟩

Share

Metrics

Record views

108

Files downloads

748