Formalizing Some ' Small ' Finite Models of Projective Geometry in Coq

Autor: Nicolas Magaud, Pascal Schreck, David Braun
Přispěvatelé: Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (ICube), Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Réseau nanophotonique et optique, Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Matériaux et nanosciences d'Alsace (FMNGE), Institut de Chimie du CNRS (INC)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Centre National de la Recherche Scientifique (CNRS)-Institut de Chimie du CNRS (INC)-Université de Strasbourg (UNISTRA)-Institut National de la Santé et de la Recherche Médicale (INSERM)-Centre National de la Recherche Scientifique (CNRS), École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et Nanosciences Grand-Est (MNGE), Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Réseau nanophotonique et optique, Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), univOAK, Archive ouverte, Magaud, Nicolas
Jazyk: angličtina
Rok vydání: 2018
Předmět:
[INFO.INFO-AI] Computer Science [cs]/Artificial Intelligence [cs.AI]
Computer science
proof automation
[INFO.INFO-GR] Computer Science [cs]/Graphics [cs.GR]
combinatorial explosion
0102 computer and information sciences
02 engineering and technology
Mathematical proof
01 natural sciences
[INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI]
projective geometry
0202 electrical engineering
electronic engineering
information engineering
Finite geometry
Coq
Axiom
Incidence (geometry)
Projective geometry
[INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC]
[INFO.INFO-SC] Computer Science [cs]/Symbolic Computation [cs.SC]
Proof assistant
[INFO.INFO-GR]Computer Science [cs]/Graphics [cs.GR]
finite inductive types
Algebra
Desargues' property
010201 computation theory & mathematics
finite geometry
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
020201 artificial intelligence & image processing
Projective plane
Combinatorial explosion
Zdroj: Proceedings of the 13th International Conference on Artificial Intelligence and Symbolic Computation (AISC'2018)
Proceedings of the 13th International Conference on Artificial Intelligence and Symbolic Computation (AISC'2018), Sep 2018, Suzhou, China
Artificial Intelligence and Symbolic Computation
13th International Conference Artificial Intelligence and Symbolic Computation ( AISC 2018 )
13th International Conference Artificial Intelligence and Symbolic Computation ( AISC 2018 ), Sep 2018, Suzhou, China. ⟨10.1007/978-3-319-99957-9⟩
Artificial Intelligence and Symbolic Computation ISBN: 9783319999562
AISC
DOI: 10.1007/978-3-319-99957-9⟩
Popis: International audience; 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.
Databáze: OpenAIRE
Externí odkaz: