用 A* 算法证明定理

Question

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

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

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

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

(b) 证明所提出的启发式是可以接受的

Answer 1

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

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

在 KB1 的所有模型中，原子 c 都是假的。如果 c 在 KB1 的模型 I 中为真，那么 a 和 b 在 I 中都为真（否则我将不是 KB1 的模型）。因为 I 在 I 中 false 为假，并且 I 中 a 和 b 为真，所以第一个子句在 I 中为假，与 I 是 KB1 的模型相矛盾。因此，c 在 KB1 的所有模型中都是错误的。这表示为 KB1 ¬c 这意味着 ¬c 在 KB1 的所有模型中为真，因此 c 在 KB1 的所有模型中为假。