min*_*t93 5 logic theorem-proving
我是二年级学生，我的离散数学 2 作业是制作一个自动定理证明器。我必须在 4 周内制作一个适用于命题逻辑的简单证明程序（假设证明始终存在）。到目前为止，我已经用谷歌搜索过，但 4 周后，那里的材料真的很难理解。谁能给我推荐一些适合初学者的书籍/网站/开源代码或一些有用的提示？先感谢您。
注意：我将其标记为将其移至计算机科学站点，因为那里的内容更多地位于 ATP 之上。
如果您能包括您所看到的内容以及为什么它对您没有帮助，那就太好了。然后我们可以找出什么可能对您更好。另外，如果您必须编写程序，那么了解您会哪些语言也会有所帮助。我对此所做的大部分工作都是使用 OCaml 或 F# 等函数式语言，或者 Prolog 或 Mercury 等逻辑语言完成的。
您是否看过约翰·哈里森 (John Harrison) 撰写的《实用逻辑和自动推理手册》(WorldCat)。我添加了(WorldCat)链接，以便您可以在当地图书馆找到这本书，而不是等待购买，这会占用您的大部分时间。
如果您仔细查看，您会发现页面底部有OCaml代码，此处有 F#，此处有 Haskell 。
如果您在维基百科上没有看到ATP或证明助手，您可能会找到一些代码和论文。