交互式数学证明系统

Question

我正在寻找一个工具(首选GUI但CLI可以工作),它允许我输入数学表达式,然后执行它们的操作,但限制我只有数学上有效的操作.此外,该工具必须能够保存会话,然后证明给定的已保存操作集是有效的.

注意:我不是在寻找一个生成校样的系统,只是检查我手动指定的步骤是否有效.

我已经使用ACL2进行类似的操作,并且它在某些情况下表现很好但是很难用于其他所有情况.

这个小项目是我的动力.它是一种D模板类型,允许求解方程.鉴于这个等式:

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

可以将任何一个符号设置为未知,并评估该表达式将导致对该变量的赋值.它的工作原理是将表达式树构建到类型中,然后使用重写规则将其转换为可以针对未知类型进行事件处理的事物.

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

Answer 1

已经提到了几个美国证明助理(通常使用LISP语法),所以这里有一个以欧洲为中心的列表来补充:

• 勒柯克

• 伊莎贝尔

• HOL4

• HOL-灯

• 开阳

所有这些都是TTY界面的臭名昭着,但Coq和Isabelle为Proof General/Emacs界面提供了很好的支持.此外,Coq还附带了CoqIDE,它基于OCaml/GTK和板载文本小部件.最近的Isabelle包括Isabelle/jEdit Prover IDE,它基于jEdit,并通过用户键入的实时提供的语义标记进行扩充.

Answer 2

ACL2是臭名昭着的 - 我们曾经说它是一个专家系统,所以只能由专家使用,他们必须向Warren Hunt,J Moore或Bob Boyer学习.你需要在ACL2中做的事情真正理解证明系统本身是如何工作的; 那么你可以在减少搜索空间的方向上"暗示"它.

但是,还有其他几种系统可以帮助解决这类问题,具体取决于您要做的事情.

如果你想使用连续数学或数论,理想的是Mathematica.问题是你可以用同样数量的钱购买二手车(除非你有资格获得学术许可,这是一个更好的交易.)

类似且免费的是Open Maxima,它是Macsyma的扩展.该页面还指出了其他几个像Axiom,我没有经验.

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