Skip to Main content Skip to Navigation
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

https://hal.inria.fr/inria-00305998
Contributor : Julien Narboux <>
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

File

ADG08-postproc-final.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

509

Files downloads

1637