Name
Abstract | ||
|---|---|---|
Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions lead to long technical proofs. In addition, when considering higher-dimensions, the amount of incidence relations (e.g. point-line, point-plane, line-plane) induce numerous technical lemmas. In this article, we investigate formalizing projective plane geometry as well as projective space geometry. We mainly focus on one of the fundamental properties of the projective space, namely Desargues property. We formally prove that it is independent of projective plane geometry axioms but can be derived from Pappus property in a two-dimensional setting. Regarding at least three-dimensional projective geometry, we present an original approach based on the notion of rank which allows to describe incidence and non-incidence relations such as equality, collinearity and coplanarity homogeneously. This approach allows to carry out proofs in a more systematic way and was successfully used to fairly easily formalize Desargues theorem in Coq. This illustrates the power and efficiency of our approach (using only ranks) to prove properties of the projective space. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1016/j.comgeo.2010.06.004 | Comput. Geom. |
Keywords | Field | DocType |
formalize desargues theorem,pappus property,projective plane geometry axiom,projective space geometry,projective space,desargues property,formalizing geometry theorem,original approach,three-dimensional projective geometry,case study,projective plane geometry,rank,projective geometry | Discrete mathematics,Projective differential geometry,Combinatorics,Non-Desarguesian plane,Projective geometry,Pure mathematics,Complex projective space,Duality (projective geometry),Projective plane,Collineation,Mathematics,Projective space | Journal |
Volume | Issue | ISSN |
45 | 8 | 0925-7721 |
Citations | PageRank | References |
4 | 0.53 | 14 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nicolas Magaud | 1 | 64 | 5.92 |
| Julien Narboux | 2 | 130 | 12.49 |
| Pascal Schreck | 3 | 213 | 23.53 |