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

Question

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

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

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

(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 中为假，与 I 是 KB1 的模型相矛盾。因此，c 在 KB1 的所有模型中都是错误的。这表示为 KB1 ¬c，这意味着 ¬c 在 KB1 的所有模型中为真，因此 c 在 KB1 的所有模型中为假。