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 条
  • [31] Computer-assisted interfacing:: On the use of computer simulation for theory construction
    Müller, G
    TOOLS AND TECHNIQUES FOR SOCIAL SCIENCE SIMULATION, 2000, : 26 - 47
  • [32] Computer-assisted proofs of the existence of a symmetry-breaking bifurcation point for the Kolmogorov problem
    Cai, Shuting
    Watanabe, Yoshitaka
    JOURNAL OF COMPUTATIONAL AND APPLIED MATHEMATICS, 2021, 395
  • [33] Computer-assisted Existence Proofs for One-dimensional Schrodinger-Poisson Systems
    Wunderlich, Jonathan
    Plum, Michael
    ACTA CYBERNETICA, 2020, 24 (03): : 373 - 391
  • [34] Reduction in Degrees of Freedom for Large-Scale Nonlinear Systems in Computer-Assisted Proofs
    Evstigneev, Nikolay M.
    Ryabkov, Oleg I.
    MATHEMATICS, 2023, 11 (20)
  • [35] Computer-Assisted Proofs for Lyapunov Stability via Sums of Squares Certificates and Constructive Analysis
    Devadze, Grigory
    Magron, Victor
    Streif, Stefan
    JOURNAL OF AUTOMATED REASONING, 2025, 69 (01)
  • [36] APPLICATION OF GRAPH-THEORY TO COMPUTER-ASSISTED MAPPING
    QI, XG
    LALL, BK
    JOURNAL OF SURVEYING ENGINEERING-ASCE, 1989, 115 (04): : 380 - 389
  • [37] COMPUTER-ASSISTED PROOFS OF EXISTENCE OF QUASI-PERIODIC SYSTEMS VIA FOURIER METHODS
    Haro, Alex
    Vidal, Eric sandin
    DISCRETE AND CONTINUOUS DYNAMICAL SYSTEMS-SERIES B, 2024,
  • [38] COMPUTER-ASSISTED EXISTENCE PROOFS FOR 2-POINT BOUNDARY-VALUE-PROBLEMS
    PLUM, M
    COMPUTING, 1991, 46 (01) : 19 - 34
  • [39] Computer-assisted Translation Teaching Based on Constructivist Theory
    Liu, Jinling
    Li, Nan
    Sun, Haibo
    PROCEEDINGS OF THE 2013 INTERNATIONAL ACADEMIC WORKSHOP ON SOCIAL SCIENCE (IAW-SC 2013), 2013, 50 : 578 - 581
  • [40] Computer-assisted proofs of existence of KAM tori in planetary dynamical models of v-And b
    Mastroianni, Rita
    Locatelli, Ugo
    COMMUNICATIONS IN NONLINEAR SCIENCE AND NUMERICAL SIMULATION, 2024, 130
12345