是否有任何软件使用 Fitch 格式（用于语言、证明和逻辑），允许放置一组特定的前提和目标，并让它向我们展示解决问题所需的完整步骤列表？
问问题
16016 次
3 回答
7
于 2011-12-29T14:29:31.827 回答
5
简短的回答：没有。
中等答案：虽然可以编写一个程序来相当容易地检查给定证明的有效性，但实际上无法做到。在命题逻辑的情况下，自动找到证明的问题是 NP 完全的（尽管它是可判定的！），并且在一阶逻辑中存在证明者永远不会停止的真定理。（不可判定）（通过哥德尔的不完备性证明）
如果你有兴趣写这样的东西，你可以尝试一下，也许让它适用于一些较小的情况，但一般来说是不可行的。
如果您正在寻找这样的东西来获得家庭作业的答案，请停止尝试。（a）你不会找到它，（b）那本书的问题很简单，而且很有趣！试一试，如果需要，请寻求帮助。当然，（c）如果你作弊，你什么也学不到。
于 2010-06-29T10:38:12.740 回答
0
考虑 OLI Carnegie Mellon 的 Apros http://www.phil.cmu.edu/projects/apros/。
于 2014-11-29T09:22:53.653 回答