Sciweavers

Share
SAC
2010
ACM

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

8 years 10 months ago
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
Tuan Minh Pham
Added 21 May 2011
Updated 21 May 2011
Type Journal
Year 2010
Where SAC
Authors Tuan Minh Pham
Comments (0)
books