演绎数据库中完整性约束的检验

计算机科学和人工智能的发展促成了更大、更复杂的知识库的构建。这些知识库容易出现矛盾，尤其在多位专家参与时。为确保在变更过程中的完整性，需要相应的处理过程。本工作从逻辑编程的角度解决该问题。完整性违例可解释为对完整性约束证明的特殊操作，其中重点关注 SLDNF 证明。我们将证明树定义为一种特殊的数据结构，并论证了此类树对 SLDNF 证明存在性的蕴含关系。证明树比 SLDNF 树更方便，并允许对证明进行面向集合的考察。它们也更清晰地呈现证明结构，从而支持进一步应用。利用该结构，我们确定了规定知识库变更何时影响完整性约束有效性的最小条件集。此外，该方法在寻找新证明时可重用旧证明的大部分内容，与以往方法相比减少了开销。