Similar triangles and orientation in plane elementary geometry for Coq-based proofs

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. Categories and Subject Descriptors I.2.3 [ Deduction and Theorem Proving]: General Terms Theory Keywords geometric theorem proving, orientation, similar triangles, formalization, Coq

• Type: Journal
• Year: 2010
• Where: SAC
• Authors: Tuan Minh Pham
• Keywords: Applied Computing, Keywords Geometric Theorem, Plane Elementary Geometry, SAC 2010, Similar Triangles