Implementing Mathematics with The Nuprl Proof Development System 论文
1986引用 994
Logic, programming, and type systemsParallel Computing and Optimization TechniquesComputability, Logic, AI Algorithms
详细信息
- 发表日期
- 1986-04-01
- 发表年份
- 1986
关键词
Logic, programming, and type systemsParallel Computing and Optimization TechniquesComputability, Logic, AI Algorithms
摘要
Problem solving is a significant part of science and mathematics and is the most intellectually significant part of programming. Solving a problem involves understanding the problem, analyzing it, exploring possible solutions, writing notes about intermediate results, reading about relevant methods, checking results, and eventually assembling a solution. Nuprl is a computer system which provides assistance with this activity. It supports the interactive creation of proofs, formulas, and terms in a formal theory of mathematics