惠誉格式校样-周围有自动求解器吗？

Question

有没有使用惠誉格式(在Language, Proof and Logic中使用)的软件，允许用户放置一组特定的前提和目标，并让它向我们显示解决问题所需的完整步骤列表？

Answer 1

简短的回答是:不。

中等答案:真的不能做到，尽管可以编写一个程序来检查给定证明的有效性。在命题逻辑的情况下，自动寻找证明的问题是NP完全的(尽管它是可判定的！)，并且在一阶逻辑中存在证明者永远不会停止的真定理。(不可判定)(通过Gödel的不完全性证明)

如果你有兴趣写这样的东西，你可以试一试，也许可以让它在一些较小的情况下工作，但这通常是不可行的。

如果你正在寻找这样的东西来获得家庭作业的答案，那就别再尝试了。(a)你不会找到它；(b)那本书中的问题很容易，而且可以很有趣！只要给他们一个尝试，并寻求帮助，如果需要。当然，(c)如果你作弊，你不会学到任何东西。

Answer 2

http://teachinglogic.liglab.fr/DN/index.php

Answer 3

考虑一下OLI Carnegie Mellon http://www.phil.cmu.edu/projects/apros/的Apros。