Computer Theorem Proving in Mathematics

被引：0
作者：
Carlos Simpson
机构：
[1] Université de Nice-Sophia Antipolis,CNRS, Laboratoire J. A. Dieudonné
来源：
Letters in Mathematical Physics | 2004年 / 69卷
关键词：
Lambda calculus; Type theory; Theorem proving; Verification; Set theory;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
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
页数：28
相关论文
共 24 条
[1]  
Fiore M.(1997)Two models of synthetic domain theory J. Pure Appl. Algebra. 116 151-162
[2]  
Rosolini G.(1998)Finite functions and the necessary use of large cardinals Ann Math 148 803-893
[3]  
Friedman H.(2003)Homotopy hyperbolic 3-manifolds are hyperbolic Ann. Math. 157 335-431
[4]  
Gabai D.(1995)Theorem in Boyer–Moore logic J. Automat. Reason. 15 217-235
[5]  
Meyerhoff G.R.(1989)The nonexistence of finite projective planes of order 10 Canad. J. Math. 41 1117-1123
[6]  
Thurston N.(1983)The nonexistence of ovals in a projective plane of order 10 Discrete Math. 45 319-321
[7]  
Kunen K.(1960)Recursive functions of symbolic expressions and their computation by machine (Part I) CACM 3 184-195
[8]  
Ramsey A.(1979)A mechanical proof of the termination of Takeuchi’s function Inform. Process. Lett. 9 176-181
[9]  
Lam C.(2002)A counterexample to a 1961 theorem in homological algebra Invent. Math. 148 397-420
[10]  
Thiel L.(1963)A. Theorem-proving on the computer J. Assoc. Comput. Mach. 10 163-174
123