On computer-assisted proofs in ordinal number theory

被引：10
|
作者：
Belinfante, JGF [1 ]
机构：
[1] Georgia Inst Technol, Sch Math, Atlanta, GA 30332 USA
来源：
JOURNAL OF AUTOMATED REASONING | 1999年 / 22卷 / 03期
关键词：
OTTER; ordinal numbers; set theory;
D O I：
10.1023/A:1006010913494
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Some basic theorems about ordinal numbers were proved using McCune's computer program OTTER, building on Quaife's modification of Godel's class theory. Our theorems are based on Isbell's elegant definition of ordinals. Neither the axiom of regularity nor the axiom of choice is used.
引用
收藏
页码：341 / 378
页数：38
相关论文
共 50 条
  • [41] Persistence of Periodic Orbits under State-dependent Delayed Perturbations: Computer-assisted Proofs
    Gimeno, Joan
    Lessard, Jean-Philippe
    James, J. D. Mireles
    Yang, Jiaqi
    SIAM JOURNAL ON APPLIED DYNAMICAL SYSTEMS, 2023, 22 (03): : 1743 - 1779
  • [42] Computer-assisted proofs of congruences for multipartitions and divisor function convolutions, based on methods of differential algebra
    Alexandru Pascadi
    The Ramanujan Journal, 2022, 57 : 1 - 36
  • [43] COMPUTER-ASSISTED SURGERY
    ADAMS, L
    KRYBUS, W
    MEYEREBRECHT, D
    RUEGER, R
    GILSBACH, JM
    MOESGES, R
    SCHLOENDORFF, G
    IEEE COMPUTER GRAPHICS AND APPLICATIONS, 1990, 10 (03) : 43 - 51
  • [44] COMPUTER-ASSISTED SPIROMETRY
    HANSEN, DJ
    TOY, VM
    DEININGER, RA
    COLLOPY, TK
    AMERICAN INDUSTRIAL HYGIENE ASSOCIATION JOURNAL, 1983, 44 (06): : 419 - 424
  • [45] COMPUTER-ASSISTED DIAGNOSIS
    HAYDEN, SP
    ANNALS OF INTERNAL MEDICINE, 1989, 111 (06) : 544 - 545
  • [46] COMPUTER-ASSISTED MANAGEMENT
    LAING, WR
    ABSTRACTS OF PAPERS OF THE AMERICAN CHEMICAL SOCIETY, 1981, 182 (AUG): : 117 - ANYL
  • [47] COMPUTER-ASSISTED WRITING
    WEBB, SS
    PERSONAL COMPUTING, 1987, 11 (11): : 19 - 19
  • [48] Computer proofs in group theory
    Yu, Yuan
    1600, (06):
  • [49] COMPUTER-ASSISTED ETCHING
    SMITH, E
    LEONARDO, 1982, 15 (03) : 229 - 230
  • [50] COMPUTER-ASSISTED MISTAKES
    LURIE, PM
    WEISS, BD
    CIVIL ENGINEERING, 1988, 58 (12): : 78 - 80
12345