Similar Triangles and Orientation in Plane Elementary Geometry for Coq-based Proofs - Archive ouverte HAL Access content directly
Conference Papers Year : 2010

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

(1)
1
Tuan Minh Pham
  • Function : Author
  • PersonId : 898947

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.
Fichier principal
Vignette du fichier
Sac-pham.pdf (317.16 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00585203 , version 1 (12-04-2011)

Identifiers

Cite

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⟩

Collections

INRIA INRIA2
256 View
316 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More