Name
Abstract | ||
|---|---|---|
We study two different descriptions of incidence projective geometry: a synthetic, mathematics-oriented one and a more practical, computation-oriented one, based on the combinatorial concept of rank of a set of points. Using both axiom systems, we prove that some specific finite planes (resp. spaces) verify the axioms of projective plane (resp. space) geometry and Desargues' property. It requires using repeated case analysis on all variables of some finite inductive data-types and leads to numerous (sub-)goals in the Coq proof assistant. We thus investigate to what extend Coq can deal with such a combinatorial explosion in the number of cases to handle. We propose some easy-to-implement but relevant proof optimizations which, combined together, lead to an efficient way to deal with such large proofs. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-319-99957-9_4 | ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION (AISC 2018) |
Keywords | Field | DocType |
Coq, Proof automation, Combinatorial explosion, Finite inductive types, Projective geometry, Finite geometry, Desargues' property | Discrete mathematics,Axiom,Projective geometry,Computer science,Mathematical proof,Projective plane,Finite geometry,Combinatorial explosion,Case analysis,Proof assistant | Conference |
Volume | ISSN | Citations |
11110 | 0302-9743 | 0 |
PageRank | References | Authors |
0.34 | 5 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| D. Braun | 1 | 22 | 1.44 |
| Nicolas Magaud | 2 | 64 | 5.92 |
| Pascal Schreck | 3 | 213 | 23.53 |