Name
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. Finally, we formally prove in Coq that Desargues' property is independent of the axioms of projective plane geometry. |
Year | Venue | Keywords |
|---|---|---|
2008 | Automated Deduction in Geometry | usual property,particular case,different axiom system,duality principle,formal model,textbook proof,projective plane geometry,duality,fano plane,projective geometry,proof assistant,projective plane,homogeneous coordinates |
Field | DocType | Citations |
Discrete mathematics,Blocking set,Non-Desarguesian plane,Projective geometry,Pencil (mathematics),Fano plane,Geometry,Duality (projective geometry),Projective plane,Mathematics,Projective space | Conference | 10 |
PageRank | References | Authors |
0.74 | 22 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nicolas Magaud | 1 | 64 | 5.92 |
| Julien Narboux | 2 | 130 | 12.49 |
| Pascal Schreck | 3 | 213 | 23.53 |