Des preuves formelles en Coq du théorème de Thalès pour les cercles

David Braun 1 Nicolas Magaud 1
1 IGG
ICube - Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie
Résumé : Le théorème de Thalès pour les cercles et sa réciproque (plus connue sous le nom de théorème du cercle circonscrit à un triangle rectangle) sont des propriétés de géométrie élémentaire enseignées dans les collèges français. Nous nous intéressons non seulement à différentes descriptions possibles de ces propriétés en Coq mais aussi aux preuves correspondantes. Nous étudions notamment comment le choix d’une représentation des objets géométriques contenus dans l’énoncé influencent les arguments de preuve. Nous présentons plusieurs approches, une basée sur des calculs d’angles, une autre basée sur la géométrie analytique et finalement deux démonstrations différentes dans l’axiomatique de Tarski en utilisant dans un cas le théorème de la droite des milieux et dans l’autre la notion de symétrie centrale et ses propriétés.
Type de document :
Communication dans un congrès
David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), 〈http://jfla.inria.fr/2015〉
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01099132
Contributeur : David Baelde <>
Soumis le : mercredi 31 décembre 2014 - 15:34:01
Dernière modification le : jeudi 29 mars 2018 - 09:10:05
Document(s) archivé(s) le : samedi 15 avril 2017 - 12:21:35

Fichier

jfla15_submission_19.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01099132, version 1

Collections

INSA-STRASBOURG | JFLA2015 | INC-CNRS | SITE-ALSACE

Citation

David Braun, Nicolas Magaud. Des preuves formelles en Coq du théorème de Thalès pour les cercles. David Baelde; Jade Alglave. Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), Jan 2015, Le Val d'Ajol, France. Actes des Vingt-sixièmes Journées Francophones des Langages Applicatifs (JFLA 2015), 〈http://jfla.inria.fr/2015〉. 〈hal-01099132〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

114

Téléchargements de fichiers

498

Contact


archive-ouverte@inria.fr