9

我正在寻找一种工具（首选 GUI，但 CLI 可以），它允许我输入数学表达式，然后对它们执行操作，但将我限制为仅在数学上有效的操作。此外，该工具必须能够保存会话并稍后证明给定的一组已保存操作是有效的。

注意：我不是在寻找生成证明的系统，只是检查我手动指定的步骤是否有效。

我已经将ACL2用于类似的操作，并且在某些情况下效果很好，但在其他所有情况下都很难使用。

这个小项目是我的动力。它是一种 D 模板类型，允许求解方程。给定这个等式：

(A * B) = C + D / F;

任何一个符号都可以设置为未知，并且评估该表达式将导致对该变量的赋值。它的工作原理是将表达式树构建到类型中，然后使用重写规则将其转换为可以为未知类型触发的东西。

我需要的是某种方法来验证重写规则。它们可以通过测试一个断言来验证，即给定一些关系是真的，另一个也是真的。

4

6 回答 6

7

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

它们都因 TTY 接口而臭名昭著，但 Coq 和 Isabelle 为 Proof General / Emacs 接口提供了良好的支持。此外，Coq 附带 CoqIDE，它基于 OCaml/GTK 和板载文本小部件。最近的 Isabelle 包括 Isabelle/jEdit Prover IDE，它基于 jEdit，并在用户键入时由 Prover 实时提供的语义标记增强。

于 2013-02-28T22:41:27.127 回答
6

ACL2 是臭名昭著的——我们曾经说它是一个专家系统，因此只能由专家使用，他们必须向 Warren Hunt、J Moore 或 Bob Boyer 学习。在 ACL2 中你需要做的是真正了解证明系统本身是如何工作的；然后你可以在减少搜索空间的方向上“提示”它。

但是，根据您要执行的操作，还有其他几个系统可以帮助解决此类问题。

如果您想使用连续数学或数论，理想的是Mathematica。问题是你可以用同样的钱买一辆二手车（除非你有资格获得学术执照，这是一个更好的交易。）

类似的，免费的，是Open Maxima，它是 Macsyma 的扩展。该页面还指向其他几个，例如 Axiom，我没有经验。

对于数学逻辑运算，有来自 SRI的PVS 。他们还有一些其他很酷的东西，比如在同一框架中进行模型检查。

于 2009-04-10T19:46:05.773 回答
2

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

人们正试图将 Mathematica、Maple 等计算机代数系统的易用性和强大功能与证明系统的逻辑严谨性结合起来。问题是：

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

  • 证明系统使用起来既困难又乏味（正如您所发现的那样）。

于 2009-04-11T07:06:29.850 回答
1

除了 Charlie Martin 的链接之外，您可能还想查看Maple。我使用此类软件的经验大约有 5 年，但我记得当时发现 Maple 比 Mathematica 更直观。

于 2009-04-10T20:00:21.090 回答
1

精益证明器是通过 JS gui 进行交互的。

于 2015-08-19T04:07:24.657 回答
0

一个古老且无人维护的系统是“Ontic”：

http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/kr/systems/ontic/0.html

于 2009-04-11T17:53:03.523 回答