惠誉格式证明 - 任何自动求解器？

Question

是否有围绕使用Fitch格式的软件（在Language, Proof and Logic中使用），允许您放置一组特定的前提和目标，并让它向我们显示解决问题所需的完整步骤列表？

Answer 1

简短的回答：第

中等答：真的不能做，但一个可以编写一个程序，很容易检查一个给定的证据的有效性。在命题逻辑的情况下，自动找到证明的问题是NP完全的（尽管它是可判定的！），并且在一阶逻辑中存在证明者永远不会停止的真正的定理。 （不可判定的）（通过哥德尔的不完整性证明）

如果你有兴趣编写这样一个东西，你可以试试它，也许它适用于一些较小的情况，但它通常是不可行的。

如果你正在寻找这样的事情来为你的家庭作业找到答案，请退出尝试。 （a）你不会找到它，（b）那本书的问题很容易，而且很有趣！只要给他们一个尝试，并在需要时寻求帮助。当然，（c）如果你作弊，你将不会学到任何东西。

Answer 2

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

Answer 3

由OLI卡内基梅隆http://www.phil.cmu.edu/projects/apros/考虑APROS。