Name
Abstract | ||
|---|---|---|
Formalizing geometry theorems in a proof assistant like Coq is challenging. As emphasized in the literature, the non-degeneracy conditions leads to 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 paper, 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. It allows to carry out proofs in a more systematic way. To validate this approach, we formalize in Coq (using only ranks) one of the fundamental theorems of the projective space, namely Desargues' theorem. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1145/1529282.1529527 | SAC |
Keywords | Field | DocType |
formalizing desargues,projective space,fundamental theorem,formalizing geometry theorem,coplanarity homogeneously,original approach,incidence relation,numerous technical lemma,non-degeneracy condition,technical proof,non-incidence relation,projective geometry,proof assistant,rank | Intersection theorem,Collinearity,Algebra,Non-Desarguesian plane,Projective geometry,Mathematical proof,Duality (projective geometry),Mathematics,Proof assistant,Projective space | Conference |
Citations | PageRank | References |
9 | 0.59 | 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 |