为什么Suppose there is an atom h ∈ C that is not a logical consequence. Let h be the first ever such atom to be added in C. There must be some clause in KB ∪ Percepts, in the form h ← a1 ∧ · · · ∧ am

这个说法是在证明 "CWA 规则" 算法的正确性时提出的。CWA 规则是一种基于一阶逻辑推理的算法，用于知识表示和推理。

在这个算法中，我们假设 C 中存在一个原子 h 不是 KB ∪ Percepts 的逻辑推论，也就是说，h 是第一个被添加到 C 中的、不是 KB ∪ Percepts 的逻辑推论。我们要证明的是，必然存在一个子句 h ← a1 ∧ · · · ∧ am，在 KB ∪ Percepts 中，使得 h 的添加是由于这个子句的缺失而导致的。

证明：

我们假设不存在这样的子句，即对于所有的子句 h ← a1 ∧ · · · ∧ am，在 KB ∪ Percepts 中，h 都是一个逻辑推论。那么，我们可以构造一个新的子句集合 C'，其中包含所有的子句 h ← a1 ∧ · · · ∧ am 和 C 中的所有原子，但是不包含 h。这样，C' 中的所有原子都是 KB ∪ Percepts 的逻辑推论，因为它们都可以从 KB ∪ Percepts 中的子句推导出来。同时，C' 中没有 h，因此 C' 和 C 有相同的模型集合。

但是，这个结论与我们的假设相矛盾，因为我们假设 C 中存在一个原子 h 不是 KB ∪ Percepts 的逻辑推论。因此，我们的假设不成立，必然存在一个子句 h ← a1 ∧ · · · ∧ am，在 KB ∪ Percepts 中，使得 h 的添加是由于这个子句的缺失而导致的。

因此，我们证明了必然存在一个子句 h ← a1 ∧ · · · ∧ am，在 KB ∪ Percepts 中，使得 h 的添加是由于这个子句的缺失而导致的。