logo标签列表

交互式数学证明系统

mathcoqtheorem-provingisabelleproof-system
9
我正在寻找一个工具（最好是GUI，但CLI也可以），允许我输入数学表达式并对其进行操作，但限制我只能使用数学上有效的操作。此外，该工具必须能够保存会话，并在以后证明给定的一组保存的操作是有效的。
注意：我不是在寻找一个系统来生成证明，只是检查我手动指定的步骤是否有效。
我已经使用ACL2执行类似的操作，在某些情况下表现良好，但在其他所有情况下都很难使用。 这个小项目是我的动力。它是一个D模板类型，允许解方程。给定这个方程：
(A * B) = C + D / F;

任何一个符号都可以被设置为未知，计算该表达式将导致对该变量的赋值。它通过将表达式树构建到类型中，然后使用重写规则将其转换为可以对未知类型进行求值的内容来工作。
我需要的是一种验证重写规则的方法。它们可以通过测试给定某个关系为真，另一个关系也为真来进行验证。
什么样的数学？抽象代数，线性代数，函数分析...？ - Pontus Gagge
@BCS，我必须承认源代码等并没有让你的意图变得非常明显。你觉得你能不能稍微总结一下你的目标是什么？ - Charlie Martin
@Charlie：b，你说得有道理。 - BCS
好的，我认为你可能需要更多地了解PVS。虽然我从未使用过它，但我已经阅读了一些文档。 - Charlie Martin
6个回答
7

已经提到了一些美国的证明助手（通常使用LISP语法），因此这里是一个以欧洲为中心的列表来补充：

它们都以TTY界面而闻名，但Coq和Isabelle为Proof General / Emacs接口提供良好支持。此外，Coq带有基于OCaml/GTK和内置文本小部件的CoqIDE。最近的Isabelle包括Isabelle/jEdit Prover IDE，它基于jEdit并通过实时提供的证明语义标记增强了编辑器功能。

有些人同时使用CoqIDE和Coq。 - t0yv0
6
ACL2是臭名昭著的——我们曾经说它是专家系统，因此只能被那些必须从Warren Hunt、J Moore或Bob Boyer学习的专家使用。在ACL2中，你需要真正地了解证明系统本身的工作原理；然后你可以“提示”它朝着减少搜索空间的方向发展。
不过，根据你想做什么，还有其他几个系统可以帮助你。
如果你想处理连续数学或数论，理想的选择是Mathematica。问题是你可以用同样的钱买一辆二手车（除非你能够获得学术许可证，这是一个更好的选择）。
类似的、免费的系统是Open Maxima，它是Macsyma的扩展。该页面还指向了几个其他系统，例如Axiom，但我没有使用过。

对于数学逻辑操作，SRI的PVS是一个不错的选择。他们在同一框架下还有一些其他很酷的功能，如模型检查。

1
除非ACL2在一定时间后放弃，否则我从未遇到搜索空间大小的问题。它只是在没有很多引理的情况下无法找到证明。 - BCS
当然可以，但这仍然是限制搜索空间的问题；它只是足够聪明，不会因为内存而过度 CONS。引理以及组织子句以获得最佳搜索的方法是我所考虑的“提示”。 - Charlie Martin
我一直希望有一个ACL2用户界面，可以精确地输入要执行的操作，并生成带有提示的ACL2代码，指导证明引擎在每个步骤上做正确的事情。你的经验可能不同，但我从未发现让ACL2为我完成任务比自己手动完成更快。更准确，是的，更快，不是。 - BCS
谁能希望拥有比EMACS缓冲区更好的用户界面呢？但说真的，ACL2并不是为了更容易而存在；Bob和J只是觉得机器检查的证明在严格意义上更可靠。如果想要更简单的选择，可以考虑Mathematica。 - Charlie Martin
2

这个领域正在进行持续的研究，称为“计算机代数中的定理证明”。

人们正在尝试将Mathematica、Maple等计算机代数系统的易用性和强大功能与证明系统的逻辑严密性相结合。问题在于：

  • 计算机代数系统不够严谨。它们往往会忘记诸如除数不能为0之类的条件。

  • 证明系统难以使用且繁琐（正如您已经发现的那样）。

正如它发生的那样，n/0问题对于我所给出的情况并不是一个问题，因为忽略它的结果恰恰是我想要发生的。 - BCS
1

Lean Prover 是通过 JS 图形用户界面进行交互的。

它还有一个 Emacs 模式。这里 是描述 lean-mode 的幻灯片。 - Anton Trunov
1
除了Charlie Martin提供的链接外，您可能还想查看Maple。我对这种软件的经验大约是5年前的，但我记得当时发现Maple比Mathematica更直观。
我会毫不犹豫地选择Maple而不是Mathematica。 - Ankur
1
根据我的编辑，我不是在寻找一个可以为我完成工作的系统（就像我记得的枫叶系统一样），而是一个可以检查我的工作的系统。 - BCS
0
网页内容由stack overflow 提供, 点击上面的
可以查看英文原文，
原文链接