Two cryptomorphic formalizations of projective incidence geometry (Q2631964)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Two cryptomorphic formalizations of projective incidence geometry |
scientific article |
Statements
Two cryptomorphic formalizations of projective incidence geometry (English)
0 references
16 May 2019
0 references
The authors formalize two different projective geometry axiomatic systems in Coq, describing the first in classical terms and the second in terms of rank from matroid theory. They prove the equivalence of these two systems in two and three dimensions. The significance of this result is that it allows for further automation for the proofs of projective geometry theorems.
0 references
automation
0 references
Coq
0 references
formalization
0 references
matroid
0 references
projective incidence geometry
0 references
ranks
0 references
0 references
