prolog - 在哪里可以找到有关 Prolog 中的证明控制的资源/信息

Question

作为作业的一部分，我被要求使用 Prolog 检查自然演绎中的证明是正确还是不正确。包含证明的名为“valid.txt”的示例文本文件如下所示：

[imp(p, q), p].
q.
[
[1, imp(p,q), premise],
[2, p, premise],
[3, q, impel(2,1)]
].```

这将是我的程序的输入，它应该对正确的证明（如上）响应“是”或“真”，对不正确的证明响应“否”或“假”。

我不知道从哪里开始。所以我的问题是，是否有一些资源可以让我了解 prolog 中的验证/控制证明。我在 prolog 中有少量编程经验，但我觉得我需要一些关于如何构建可以验证证明的程序的具体说明。我一直在寻找教科书和网站，但找不到任何可以帮助我的东西。

最后，我的程序可能类似于这样：检查包含假设的逻辑序列是否有效

因为这是我第一次在这里提问，如果我错过了什么，我深表歉意。

标签： prologproof

Answer 1

在某种程度上，我完全理解近距离投票、评论等，但另一方面，我完全可以理解你对故事的看法。

意识到我确实认为你的问题只是在此处允许的错误方面，但并没有太多，以至于其他新人不会做同样的事情。

此处不允许提出图书推荐问题。通常一本书推荐会被认为是主观的，但是当只有一两本书符合要求时，怎么可能是主观的。

John Harrison ( WorldCat ) ( Amazon ) ( Webpage )的“实用逻辑和自动推理手册”

注意：本书使用编程语言 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 的更简单版本。

这些链接应该让您了解工作应用程序，这些都属于自动定理证明这一更广泛的主题，这与证明助手不同。