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 条
12345