Similar Triangles and Orientation in Plane Elementary Geometry for Coq-based Proofs

Tuan Minh Pham 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In plane elementary geometry, the concept of similar triangles not only forms an important foundation for trigonometry, but it also can be used to solve many geometric problems. The notion of orientation allows us to remove the usual ambiguities in presentation of object. In this paper, we present the formalization of these notions in Coq. We also introduce their properties and how they are applied to the proof of two theorems: the Ptolemy's theorem and the Intersecting Chords theorem.
Type de document :
Article dans une revue
SAC '10 Proceedings of the 2010 ACM Symposium on Applied Computing, ACM Proceeding, 2010
Liste complète des métadonnées

Littérature citée [4 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00585203
Contributeur : Tuan Minh Pham <>
Soumis le : mardi 12 avril 2011 - 10:26:33
Dernière modification le : lundi 5 octobre 2015 - 16:57:30
Document(s) archivé(s) le : mercredi 13 juillet 2011 - 02:33:24

Fichier

Sac-pham.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00585203, version 1

Collections

Citation

Tuan Minh Pham. Similar Triangles and Orientation in Plane Elementary Geometry for Coq-based Proofs. SAC '10 Proceedings of the 2010 ACM Symposium on Applied Computing, ACM Proceeding, 2010. 〈inria-00585203〉

Partager

Métriques

Consultations de la notice

422

Téléchargements de fichiers

276