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

Tuan Minh Pham (1)

1 MARELLE - Mathematical, Reasoning and Software

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.

Domaines: Logique en informatique [cs.LO]

Tuan Minh Pham. Similar Triangles and Orientation in Plane Elementary Geometry for Coq-based Proofs. SAC 2010 - 25th ACM International Symposium on Applied Computing, Mar 2010, Sierre, Switzerland. ⟨10.1145/1774088.1774358⟩. ⟨inria-00585203⟩