Skip to Main content Skip to Navigation
New interface
Conference papers

Formalizing Projective Plane Geometry in Coq

Abstract : We investigate how projective plane geometry can be formalized in a proof assistant such as Coq. Such a formalization increases the reliability of textbook proofs whose details and particular cases are often overlooked and left to the reader as exercises. Projective plane geometry is described through two different axiom systems which are formally proved equivalent. Usual properties such as decidability of equality of points (and lines) are then proved in a constructive way. The duality principle as well as formal models of projective plane geometry are then studied and implemented in Coq.
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download
Contributor : Julien Narboux Connect in order to contact the contributor
Submitted on : Monday, June 28, 2010 - 4:37:32 PM
Last modification on : Tuesday, December 8, 2020 - 9:41:58 AM
Long-term archiving on: : Thursday, December 1, 2016 - 6:06:24 AM


Files produced by the author(s)




Nicolas Magaud, Julien Narboux, Pascal Schreck. Formalizing Projective Plane Geometry in Coq. Post-proceedings of Automated Deduction in Geometry (ADG) 2008, Thomas Sturm, Sep 2008, Shanghai, China. pp.141-162, ⟨10.1007/978-3-642-21046-4⟩. ⟨inria-00305998v3⟩



Record views


Files downloads