Proof-checking Euclid

Autor: Freek Wiedijk, Michael Beeson, Julien Narboux
Přispěvatelé: San Jose State University [San Jose] (SJSU), Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (ICube), É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), Institute for Computing and Information Sciences [Nijmegen] (ICIS), Radboud University [Nijmegen], San Jose State University [San José] (SJSU), 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), Radboud university [Nijmegen]
Rok vydání: 2019
Předmět:
FOS: Computer and information sciences
Computer Science - Logic in Computer Science
Correctness
formalization
Computer science
02 engineering and technology
Mathematical proof
Fragment (logic)
Artificial Intelligence
Simple (abstract algebra)
Euclidean geometry
ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION
HOL-Light
0202 electrical engineering
electronic engineering
information engineering
Calculus
Hol light
Software Science
Coq
Axiom
[INFO.INFO-MS]Computer Science [cs]/Mathematical Software [cs.MS]
Applied Mathematics
Euclid
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
[INFO.INFO-IA]Computer Science [cs]/Computer Aided Engineering
Logic in Computer Science (cs.LO)
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Proof checking
F.4.1
ITP
020201 artificial intelligence & image processing
Software_PROGRAMMINGLANGUAGES
03A99
Zdroj: Annals of Mathematics and Artificial Intelligence
Annals of Mathematics and Artificial Intelligence, 2019, pp.53. ⟨10.1007/s10472-018-9606-x⟩
Annals of Mathematics and Artificial Intelligence, 85, 2-4, pp. 213-257
Annals of Mathematics and Artificial Intelligence, Springer Verlag, 2019, pp.53. ⟨10.1007/s10472-018-9606-x⟩
Annals of Mathematics and Artificial Intelligence, 85, 213-257
ISSN: 1012-2443
1573-7470
DOI: 10.1007/s10472-018-9606-x⟩
Popis: We used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. We used axioms as close as possible to those of Euclid, in a language closely related to that used in Tarski's formal geometry. We used proofs as close as possible to those given by Euclid, but filling Euclid's gaps and correcting errors. Euclid Book I has 48 propositions, we proved 235 theorems. The extras were partly "Book Zero", preliminaries of a very fundamental nature, partly propositions that Euclid omitted but were used implicitly, partly advanced theorems that we found necessary to fill Euclid's gaps, and partly just variants of Euclid's propositions. We wrote these proofs in a simple fragment of first-order logic corresponding to Euclid's logic, debugged them using a custom software tool, and then checked them in the well-known and trusted proof checkers HOL Light and Coq.
53 pages
Databáze: OpenAIRE
Externí odkaz: