Euclid after Computer Proof-Checking

被引：3
|
作者：
Beeson, Michael [1 ]
机构：
[1] San Jose State Univ, Dept Math, One Washington Sq, San Jose, CA 95192 USA
来源：
AMERICAN MATHEMATICAL MONTHLY | 2022年 / 129卷 / 07期
关键词：
GEOMETRY;
D O I：
10.1080/00029890.2022.2069985
中图分类号：
O1 [数学];
学科分类号：
0701 ; 070101 ;
摘要：
Euclid pioneered the concept of a mathematical theory developed from axioms by a series of justified proof steps. From the outset there were critics and improvers. In this century the use of computers to check proofs for correctness sets a new standard of rigor. How does Euclid stand up under such an examination? And what does the exercise have to teach us about geometry. mathematical foundations, and the relation of logic to truth?
引用
收藏
页码：623 / 646
页数：24
相关论文
共 50 条
  • [1] Proof-checking Euclid
    Beeson, Michael
    Narboux, Julien
    Wiedijk, Freek
    [J]. ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2019, 85 (2-4) : 213 - 257
  • [2] Proof-checking Euclid
    Michael Beeson
    Julien Narboux
    Freek Wiedijk
    [J]. Annals of Mathematics and Artificial Intelligence, 2019, 85 : 213 - 257
  • [3] Interactive and probabilistic proof-checking
    Trevisan, L
    [J]. ANNALS OF PURE AND APPLIED LOGIC, 2000, 104 (1-3) : 325 - 342
  • [4] Proof-checking protocols using bisimulations
    Röckl, C
    Esparza, J
    [J]. CONCUR'99: CONCURRENCY THEORY, 1999, 1664 : 525 - 540
  • [5] A FORMALISM FOR PRIMITIVE LOGIC AND MECHANICAL PROOF-CHECKING
    ONO, K
    [J]. NAGOYA MATHEMATICAL JOURNAL, 1966, 26 (FEB) : 195 - &
  • [6] READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking
    Wenzel, Makarius
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (118): : 57 - 71
  • [7] A two-level approach towards lean proof-checking
    Barthe, G
    Ruys, M
    Barendregt, H
    [J]. TYPES FOR PROOFS AND PROGRAMS, 1996, 1158 : 16 - 35
  • [8] THE PROOF-CHECKING COMPONENT FOR THE PLEATS PROGRAMMING SYSTEM ENABLING SPECIFICATION OF THEORIES
    CYBULKA, J
    BARTOSZEK, J
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1986, 215 : 149 - 155
  • [9] Reconstruction of the Frauenkirche Dresden, structural proof-checking using a complete 3D FE-model
    Peter, J
    Hertenstein, M
    [J]. STRUCTURAL STUDIES, REPAIRS AND MAINTENANCE OF HISTORICAL BUILDINGS VI, 1999, 6 : 843 - 854
  • [10] Reconstruction of the Frauenkirche Dresden: Structural proof-checking using a complete 3D FE-model
    Peter, J
    Hertenstein, M
    [J]. REVIVAL OF DRESDEN, 2000, 7 : 185 - 196
12345