artificial-intelligence - 用 A* 算法证明定理

Question

我正在准备硕士的期末考试，这是过去考试的问题，我真的很困惑，不知道从哪里开始。

我的想法是可采启发式是解析规则，然后证明解析规则是可采的，对吗？如果是这样，要证明决议规则是可接受的，我应该从哪里开始？感谢您的帮助。

考虑一个定理证明器应用程序。 A* 算法可用于搜索最简单的
(最短)证明。假设已知公理和定理被表示为命题逻辑中 Horn 子句的知识库，并且证明者使用反向链接。

(a) 提出一个可接受的启发式方法。

(b) 证明提议的启发式方法是可接受的

Answer 1

是的，定理证明意味着它是一种解决方案。
Horn 子句是确定子句或完整性约束。也就是说，Horn 子句的头部要么是假原子，要么是正常原子。
完整性约束是以下形式的子句
false←a1∧...∧ak。
完整性约束允许系统证明在知识库的所有模型中某些原子的结合是错误的——也就是说，证明原子的否定的析取
Horn 子句知识库可以暗示原子的否定
例如:考虑知识库 KB1:

false←a∧b.
a←c.
b←c.

在 KB1 的所有模型中，原子 c 都是假的。如果 c 在 KB1 的模型 I 中为真，则 a 和 b 在 I 中都为真(否则我将不是 KB1 的模型)。因为假在 I 中为假，a 和 b 在 I 中为真，所以第一个子句在 I 中为假，与作为 KB1 模型的 I 相矛盾。因此，在 KB1 的所有模型中，c 都是假的。这表示为
KB1 ¬c
这意味着 ¬c 在 KB1 的所有模型中为真，因此 c 在 KB1 的所有模型中为假。