基于 SE-模型的语义规则更新的兴衰

基于稳定模型语义的逻辑程序（或答案集程序）提供了一种富有表现力的基于规则的知识表示框架，具有形式化、声明式且易于理解的语义。然而，处理规则库的演化仍然是一个 largely open problem。研究表明，当直接将用于信念变化的 AGM 框架应用于具有非单调语义（如稳定模型）的逻辑程序时，会产生不恰当的结果。迄今为止开发的解决此问题的方法，提出了基于操作程序和规则句法结构的更新语义。最近，AGM 修正已成功应用于基于 SE-模型的逻辑程序的更具表现力的语义刻画。这是重要的一步，因为它将焦点从规则库的句法表示演化转移到了其语义内容的演化。在本文中，我们借用信念更新领域的成果来解决更新（而非修正）答案集程序的问题。我们证明了一个表示定理，使得能够构造性地定义任何满足一组公设的算子，这些公设源自 Katsuno 和 Mendelzon 关于信念更新的公设。基于该定理，我们定义了一个特定算子，考察了其计算复杂性，并将该算子的行为与文献中的句法规则更新语义进行了比较。或许令人惊讶的是，我们揭示了所有基于 Katsuno 和 Mendelzon 更新方法及 SE-模型的规则更新算子都存在一个严重缺陷。