稳定模型语义的扩展与实现

我们发展了一种用于计算逻辑程序稳定模型语义的算法。证明可以将语义和算法扩展以处理新的更具表达力的规则类型。特别强调了高效实现技术的使用。具体提出了一种 lookahead 实现方法，该方法可安全地避免对每个文字都进行失败测试，从而使 lookahead 的使用变得可行。此外，推导出一个良好的启发式方法，原则是应最小化搜索空间。由于缺乏竞争性的算法和实现来计算稳定模型，该系统被与三个满足性求解器进行比较。这表明可以通过打破平局来改进启发式方法，但也留下了如何打破平局的问题。它还表明，稳定模型语义的更具表达力的规则使得当问题具有更紧凑的逻辑程序表示时，稳定模型语义明显优于命题逻辑。当且仅当逻辑程序表示比常规形式更紧凑时，合取normal form 表示才不会更紧凑。