logic - 自动定理证明程序 - 从哪里开始？

Question

关闭。这个问题是off-topic .它目前不接受答案。












想改进这个问题？ Update the question所以它是on-topic对于堆栈溢出。

9年前关闭。




Improve this question




我是一名二年级学生，我的离散数学 2 任务是制作一个自动定理证明器。我必须在 4 周内制作一个适用于命题逻辑的简单证明程序(假设证明始终存在)。到目前为止，我已经用谷歌搜索了，但那里的 Material 在 4 周内真的很难理解。谁能推荐我一些适合初学者的书籍/网站/开源代码或一些有用的提示？先感谢您。

Answer 1

注意:我将其标记为将其移至计算机科学站点，因为它们更多地位于那里的 ATP 之上。

如果您可以包含您所查看的内容以及它为什么对您没有帮助，那就太好了。然后我们可以找出什么可能对你更好。此外，如果您必须编写程序，那么了解您所知道的语言会有所帮助。我对此所做的大部分工作都是使用诸如 OCaml 或 F# 之类的函数式语言或诸如 Prolog 或 Mercury 之类的逻辑语言来完成的。

你见过“Handbook of Practical Logic and Automated Reasoning”(WorldCat)通过约翰哈里森。我包括了(WorldCat)链接，这样您就可以在本地图书馆找到这本书，而不是等待购买它，这会占用您大部分时间。

如果你看你会发现OCaml页面底部的代码和 F# here和 Haskell here .

如果您还没有看到 ATP或 Proof Assistant在 Wikipedia，您可能会得到一些代码和论文的线索。