Two cryptomorphic formalizations of projective incidence geometry (Q2631964)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: Two cryptomorphic formalizations of projective incidence geometry |
scientific article; zbMATH DE number 7055782
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Two cryptomorphic formalizations of projective incidence geometry |
scientific article; zbMATH DE number 7055782 |
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
0.886109471321106
0 references
0.8546350598335266
0 references
0.8467321991920471
0 references
0.8360019326210022
0 references
0.8137697577476501
0 references
