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.
Type de document :
Communication dans un congrès
Thomas Sturm. Post-proceedings of Automated Deduction in Geometry (ADG) 2008, Sep 2008, Shanghai, China. Springer, 6301, pp.141-162, 2011, LNAI. 〈10.1007/978-3-642-21046-4〉
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00305998
Contributeur : Julien Narboux <>
Soumis le : lundi 28 juin 2010 - 16:37:32
Dernière modification le : jeudi 11 janvier 2018 - 06:20:29
Document(s) archivé(s) le : jeudi 1 décembre 2016 - 06:06:24

Fichier

ADG08-postproc-final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

176

Téléchargements de fichiers

469