知识的增量重编译

Selman 和 Kautz (1991, 1996) 提出用 Horn 公式从上方和下方逼近一般公式（分别为其 Horn 包络和 Horn 核），作为“知识编译”的一种形式，以支持快速近似推理；不利的一面是，该方案是静态的，即它不支持更新，并且具有 Kavvadias、Papadimitriou 和 Sideri (1993) 指出的某些复杂性缺陷。另一方面，正如 Eiter 和 Gottlob (1992) 所指出并在本文中进一步证明的那样，文献中提出的用于理论更新与修正的许多框架和方案受到严重的复杂性理论障碍的困扰，即使在 Horn 情况下也是如此。更根本的是，这些方案是非归纳的，因为它们可能在单次更新中丧失所表示公式集的任何正面性质（小规模、Horn 结构等）。在本文中，我们提出了一种新方案——增量重编译，它结合了 Horn 逼近与基于模型的更新；该方案是归纳的且非常高效，免除了其组成部分所面临的问题。一个公式集由上下 Horn 逼近表示。为了更新，我们将上 Horn 公式替换为其最小变更更新的 Horn 包络，同样地将下 Horn 公式替换为其更新的 Horn 核；使该方案成为可能的关键事实是，当底层公式是 Horn 公式被一个子句进行最小变更更新的结果时，Horn 包络和核易于计算。我们推测对于更复杂的更新也可能存在高效的算法。