ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 24/9 - 2005  - pp.1113-1138  - doi:10.3166/tsi.24.1113-1138
TITRE
Formalisation en Coq et visualisation d'un cours de géométrie pour le lycée

RÉSUMÉ
Enseigner les mathématiques aux élèves de lycée en utilisant la démonstration assistée par ordinateur devient un objectif accessible dans un futur proche. Nous présentons dans cet article une formalisation en Coq de la géométrie enseignée au lycée ayant la particularité de présenter des définitions, théorèmes et preuves très proches de ceux donnés dans les cours de mathématiques. Pour rendre les textes formels accessibles aux élèves, nous utilisons une interface graphique et un outil de construction automatique de figure dynamique. Nous présentons dans cet article plusieurs exemples d'énoncés, démonstrations et figures correspondantes puis abordons les difficultés rencontrées dans ce travail.


ABSTRACT
Teaching high-school mathematics using a general theorem prover becomes a reachable goal for the near future. In this article, we present a library dealing with geometry in Coq. This library is dedicated to high-school teaching. We stress on using a graphical interface and a drawing tool which ease the accessibility to formal statements. We present some significant examples of statements with figures and proofs developed with Coq. Then we discuss the difficulties encountered in this work.


AUTEUR(S)
Frédérique GUILHOT

MOTS-CLÉS
géométrie, assistant à la preuve, enseignement, logiciel de géométrie, Coq

KEYWORDS
geometry, theorem prover, teaching, drawing tool, Coq

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (480 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier