仅为数学证明助理
仅为数学证明助理
提问于 2015-02-16 09:45:53
大多数验证助手都是带有依赖类型的函数式编程语言。他们可以证明程序/算法。相反，我感兴趣的是最适合数学的证明助手(例如微积分)。你能推荐一个吗？我听说过Mizar，但我不喜欢源代码已经关闭，但如果它对数学最好，我将使用它。像Agda和Idris这样的新语言对数学证明有多好？
回答 1
Stack Overflow用户
回答已采纳
发布于 2015-02-16 14:37:48
Coq拥有涵盖实际分析的广泛库。人们想到了各种事态发展：
- standard library和在其基础上构建的项目，如现已失效的coqtail项目1或最近的coquelicot。所有这些都依赖于reals presented here的公理定义。
- 一个更有建设性的方法是由the C-CoRN项目提供的，它从实际构建reals开始。
另一种解决方法是转向非标准分析。这就是使用ACL2的人一直在做的事情。
要了解该领域的更一般视图，您可能应该阅读参与coquelicot项目的人员的this survey paper。
1充分披露:我参与了那个项目。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/28538510
复制相关文章
相似问题
腾讯云开发者
