作为作业的一部分，我被要求使用Prolog检查自然推导中的证明是正确的还是不正确的。一个名为"valid.txt"的包含证明的示例文本文件如下所示：
[imp(p, q), p].
q.
[
[1, imp(p,q), premise],
[2, p, premise],
[3, q, impel(2,1)]
].```
这将是我的程序的输入，它应该对正确的证明(如上所述(回答"是"或"真"，对不正确的证明回答"否"或"假"。
我不知道从哪里开始。所以我的问题是，是否有一些资源可以让我学习如何在prolog中验证/控制证明。我在prolog中有一些编程经验，但我觉得我需要一些关于如何构建一个可以验证证明的程序的具体说明。我找过课本和网站，但找不到任何能帮助我的东西。
最后，我的程序应该类似于这样：检查其中包含假设的逻辑序列是否是有效的
由于这是我第一次在这里提问，如果我遗漏了什么，我深表歉意。
在某种程度上，我完全理解势均力敌的投票、评论等，但在另一方面，我完全可以理解你的观点。
要意识到，我确实认为你的问题几乎没有站在这里允许的错误一边，但也不至于让其他新来者也做同样的事情。
这里不允许提出图书推荐问题。通常情况下，书籍推荐会被视为主观的，但当只有一两本书符合要求时，它怎么可能是主观的呢。
约翰·哈里森(WorldCat((亚马逊((网页(的《实用逻辑和自动推理手册》
注意：本书使用编程语言OCaml，但实现了Prolog的一个子集。此外，这本书使用了一种特定于领域的语言，并实现了一个解析器。
这本书显然远远超出了你的需求，所以你不需要阅读整本书。
你可能只需要这个在prop.ml 中找到的
let rec eval fm v =
match fm with
False -> false
| True -> true
| Atom(x) -> v(x)
| Not(p) -> not(eval p v)
| And(p,q) -> (eval p v) & (eval q v)
| Or(p,q) -> (eval p v) or (eval q v)
| Imp(p,q) -> not(eval p v) or (eval q v)
| Iff(p,q) -> (eval p v) = (eval q v);;
示例查询
tautology <<p / q ==> q / (p <=> q)>>;;
这本书更详细地介绍了一个功能更丰富的版本HOL Light的源代码，它是HOL的一个更简单的版本。
这些链接应该让你进入工作应用程序的棒球场，这些都属于自动化定理证明的更广泛主题，这与证明助手不同。