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

Question

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

Answer 1

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

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

您看过John Harrison的“实用逻辑和自动推理手册” （WorldCat）吗？我添加了（WorldCat）链接，这样您就可以在当地图书馆找到这本书，而不是等待购买它，这会占用您大部分时间。

如果你看一下，你会在页面底部找到OCaml代码，这里是 F# ，这里是Haskell 。

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