Computer theorem proving in mathematics

被引：5
作者：
Simpson, C [1 ]
机构：
[1] Univ Nice, CNRS, Lab JA Dieudonne, F-06108 Nice 2, France
来源：
LETTERS IN MATHEMATICAL PHYSICS | 2004年 / 69卷 / 1期
关键词：
lambda calculus; type theory; theorem proving; verification; set theory;
D O I：
10.1007/s11005-004-0607-9
中图分类号：
O4 [物理学];
学科分类号：
0702 ;
摘要：
We give an overview of issues surrounding computer-verified theorem proving in the standard pure-mathematical context. This includes the basic reasons why it should be interesting to pure mathematicians, some history, natural desiderata for a useful system, viewpoints on what kind of logic to use, a short explanation of how things work, an overview of different options for encoding sets, and perspectives on future developments.
引用
收藏
页码：287 / 315
页数：29
相关论文
共 100 条
[1]  
ACZEL P, 1977, LOGIC C 77
[2]  
Agerholm S., 1995, Higher Order Logic Theorem Proving and Its Applications. 8th International Workshop. Proceedings, P32
[3]  
ALEXANDRE G, AXIOMATISATION INTUI
[4]  
Alonso Tarrio L., 1999, CONT MATH, V244
[5]  
ALTENKIRCH T, IN PRESS WCGP 2002
[6]  
[Anonymous], 1994, AUTOMATH SYSTEM
[7]  
[Anonymous], 1991, AUTOMATED REASONING
[8]  
[Anonymous], 1984, STUDIES PROOF THEORY
[9]  
BARRAS B, PARADOXES SET THEORY
[10]  
BERTOT Y, IN PRESS COQ ART
12345678910