交互式数学证明系统
我正在寻找一种工具（首选 GUI，但 CLI 也可以），它允许我输入数学表达式，然后对其进行操作，但限制我只能进行数学上有效的运算。 此外，该工具必须能够保存会话，并在以后证明给定的一组已保存操作是有效的。
注意：我不是寻找一个系统来生成证明，只是检查我手动指定的步骤是否有效。
我已经使用< a href="http://en.wikipedia.org/wiki/ACL2" rel="nofollow noreferrer">ACL2 用于类似的操作，它在某些情况下效果很好，但很难用于其他所有情况。
这个小项目是我的动力。 这是一个 D 模板类型，允许求解方程。 给定这个等式：
(A * B) = C + D / F;
任何一个符号都可以设置为未知，并且评估该表达式将导致对该变量的赋值。 它的工作原理是在类型中构建表达式树，然后使用重写规则将其转换为可以最终用于未知类型的东西。
我需要的是某种方法来验证重写规则。 它们可以通过测试断言来验证，即给定某个关系为真，另一个关系也为真。
I'm looking for a tool (GUI preferred but CLI would work) that allows me to input math expressions and then perform manipulations of them but restricts me to only mathematically valid operations. Also, the tool must be able to save a session and later prove that the given set of saved operations is valid.
Note: I am Not looking for a system to generate proofs, only that check that the steps I manually specify are valid.
I have used ACL2 for similar operations and it does well for some cases but it is very hard to use for everything else.
This little project is my motivation. It is a D template type that allows for equation solving. Given this equation:
(A * B) = C + D / F;
Any one of the symbols can be set as unknown and evaluating that expression will result an an assignment to that variable. It works by building expression trees into the type and then using rewrite rules to convert it to something that can be eventuated for the unknown type.
What I need is some way to validate the rewrite rule. They can be validated by testing the assertion that given some relation is true, another one is also.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（6）
已经提到了几个美国证明助手（通常使用 LISP 语法），因此这里有一个以欧洲为中心的列表来补充：
Coq
伊莎贝尔
HOL4
HOL-Light
米扎尔
它们都因 TTY 界面而臭名昭著，但 Coq 和 Isabelle 对 Proof General / Emacs 界面提供了良好的支持。 此外，Coq 附带了 CoqIDE，它基于 OCaml/GTK，是一个板载文本小部件。 最近的 Isabelle 包括 Isabelle/jEdit Prover IDE，它基于 jEdit，并通过证明者在用户键入时实时提供的语义标记进行了增强。
Several American proof assistants were mentioned already (usually with LISP syntax), so here is a Europe-centric list to complement that:
Coq
Isabelle
HOL4
HOL-Light
Mizar
All of them are notorious for TTY interfaces, but Coq and Isabelle provide good support for the Proof General / Emacs interface. Moreover, Coq comes with CoqIDE, which is based on OCaml/GTK an the on-board text widget. Recent Isabelle includes the Isabelle/jEdit Prover IDE, which is based on jEdit and augmented by semantic markup provided by the prover in real-time as the user types.
ACL2 是臭名昭著的——我们过去常说它是一个专家系统，因此只能由专家使用，他们必须向 Warren Hunt、J Moore 或 Bob Boyer 学习。 在 ACL2 中你需要做的就是真正理解证明系统本身是如何工作的； 然后你可以“提示”它的方向，以减少搜索空间。
不过，还有其他几个系统可以帮助解决此类问题，具体取决于您想要做什么。
如果您想使用连续数学或数论，理想的选择是 Mathematica。 问题是你可以用同样的钱购买一辆二手车（除非你有资格获得学术执照，这是一个更好的交易。）
类似的、免费的东西是打开 Maxima，它是 Macsyma 的扩展。 该页面还指向其他几个页面，例如 Axiom，我对此没有任何经验。
对于数学逻辑运算，可以使用 SRI 的 PVS。 他们还有一些其他很酷的东西，比如在同一框架中进行模型检查。
ACL2 is notorious -- we used to say it was an expert system, and so could only be used by experts, who had to learn from Warren Hunt, J Moore, or Bob Boyer. The thing you need to do in ACL2 is really really understand how the proof system itself works; then you can "hint" it in directions that reduce the search space.
There are several other systems that can help with this kind of thing, though, depending on what you're trying to do.
If you want to work with continuous math or number theory, the ideal is Mathematica. Problem is you can buy a used car for the same amount of money (unless you can qualify for an academic license, a far better deal.)
Something similar, and free, is Open Maxima, which is an extension of Macsyma. That page also points to several others like Axiom, that I've got no experience with.
For mathematical logic operations, there's PVS from SRI. They've got some other cool stuff like model-checking in the same framework.
该领域正在进行的研究，称为“计算机代数中的定理证明”。
人们试图将 Mathematica、Maple 等计算机代数系统的易用性和强大功能与证明系统的逻辑严谨性结合起来。 问题是：
计算机代数系统并不严格。 他们往往会忘记一些附带条件，例如除数不能为 0。
证明系统使用起来困难且乏味（正如您所发现的）。
There's ongoing research in this area, it's called "Theorem proving in computer algebra".
People are trying to merge the ease of use and power of computer algebra systems like Mathematica, Maple, ... with the logical rigor of proof systems. The problems are:
Computer algebra systems are not rigorous. They tend to forget side conditions such as that a divisor must not be 0.
The proof systems are hard and tedious to use (as you have discovered).
除了 Charlie Martin 的链接之外，您可能还想查看 Maple。 我使用此类软件的经验大约有 5 年，但我记得当时发现 Maple 比 Mathematica 直观得多。
In addition to what Charlie Martin's links, you may also want to check out Maple. My experience with such software is about 5 years old, but I recall at the time finding Maple to be much more intuitive than Mathematica.
精益证明通过 JS gui 进行交互。
The lean prover is interactive through a JS gui.
一个旧的且未维护的系统是“Ontic”：
An old and unmaintained system is 'Ontic':
http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/kr/systems/ontic/0.html