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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [4 references]  Display  Hide  Download

https://hal.inria.fr/inria-00585203
Contributor : Tuan Minh Pham <>
Submitted on : Tuesday, April 12, 2011 - 10:26:33 AM
Last modification on : Thursday, January 11, 2018 - 4:22:49 PM
Long-term archiving on : Wednesday, July 13, 2011 - 2:33:24 AM

File

Sac-pham.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

559

Files downloads

423