A Synthetic Proof of Pappus’ Theorem in Tarski’s Geometry

Autor: Gabriel Braun, Julien Narboux
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)
Rok vydání: 2016
Předmět:
geometry
formalization
Informatique [cs]/Logiciel mathématique [cs.MS]
Absolute geometry
Geometry
0102 computer and information sciences
02 engineering and technology
01 natural sciences
neutral geometry
Artificial Intelligence
Euclidean geometry
0202 electrical engineering
electronic engineering
information engineering
Ordered geometry
Foundations of geometry
Pappus theorem
Synthetic geometry
[INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS]
Mathematics
synthetic proof
Parallel postulate
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Informatique [cs]/Ingénierie assistée par ordinateur
Informatique [cs]/Logique en informatique [cs.LO]
[INFO.INFO-IA]Computer Science [cs]/Computer Aided Engineering
Tarski's axioms
Computational Theory and Mathematics
010201 computation theory & mathematics
coq
020201 artificial intelligence & image processing
Software
Analytic proof
Zdroj: Journal of Automated Reasoning
Journal of Automated Reasoning, Springer Verlag, 2017, 58 (2), pp.23. ⟨10.1007/s10817-016-9374-4⟩
Journal of Automated Reasoning, 2017, 58 (2), pp.23. ⟨10.1007/s10817-016-9374-4⟩
ISSN: 1573-0670
0168-7433
DOI: 10.1007/s10817-016-9374-4
Popis: International audience; In this paper, we report on the formalization of a synthetic proof of Pappus' theorem. We provide two versions of the theorem: the first one is proved in neutral geometry (without assuming the parallel postulate), the second (usual) version is proved in Euclidean geometry. The proof that we formalize is the one presented by Hilbert in The Foundations of Geometry which has been detailed by Schwabhäuser , Szmielew and Tarski in part I of Metamathematische Methoden in der Geometrie. We highlight the steps which are still missing in this later version. The proofs are checked formally using the Coq proof assistant. Our proofs are based on Tarski's axiom system for geometry without any continuity axiom. This theorem is an important milestone toward obtaining the arithmetization of geometry which will allow us to provide a connection between analytic and synthetic geometry.
Databáze: OpenAIRE
Externí odkaz: