Medium Answer: Can't really be done, though one could write a program to check the validity of a given proof fairly easily. In the case of propositional logic, the problem of automatically finding a proof is NP-complete (though it is decidable!), and in first order logic there are true theorems for which the prover would never stop. (undecidable) (via Gödel's incompleteness proof)
If you're interested in writing such a thing, you can take a stab at it, and maybe get it to work for some smaller cases, but it's not doable in general.
If you're looking for such a thing to get answers for your homework, quit trying. (a) you won't find it and (b) the problems from that book are pretty easy, and can be fun! Just give them a try, and seek out help if needed. and, of course, (c) you won't learn anything if you cheat.
发布评论
评论（3）
http://teachinglogic.liglab.fr/DN/index.php
http://teachinglogic.liglab.fr/DN/index.php
简短的回答：不。
中等的回答：实际上不可能做到，尽管人们可以编写一个程序来相当容易地检查给定证明的有效性。在命题逻辑的情况下，自动找到证明的问题是 NP 完全的（尽管它是可判定的！），并且在一阶逻辑中，存在证明者永远不会停止的真定理。 （不可判定）（通过哥德尔的不完备性证明）
如果你有兴趣写这样的东西，你可以尝试一下，也许让它适用于一些较小的情况，但一般来说这是不可行的。
如果您正在寻找这样的东西来获得作业的答案，请停止尝试。 (a) 你不会找到它，(b) 那本书中的问题非常简单，而且很有趣！尝试一下，并在需要时寻求帮助。当然，(c) 如果你作弊，你就不会学到任何东西。
Short answer: No.
Medium Answer: Can't really be done, though one could write a program to check the validity of a given proof fairly easily. In the case of propositional logic, the problem of automatically finding a proof is NP-complete (though it is decidable!), and in first order logic there are true theorems for which the prover would never stop. (undecidable) (via Gödel's incompleteness proof)
If you're interested in writing such a thing, you can take a stab at it, and maybe get it to work for some smaller cases, but it's not doable in general.
If you're looking for such a thing to get answers for your homework, quit trying. (a) you won't find it and (b) the problems from that book are pretty easy, and can be fun! Just give them a try, and seek out help if needed. and, of course, (c) you won't learn anything if you cheat.
考虑 OLI 卡内基梅隆大学的 Apros http://www.phil.cmu.edu/projects/apros/ 。
Consider Apros by OLI Carnegie Mellon http://www.phil.cmu.edu/projects/apros/ .