逻辑程序带否定-as-失败的最小模型语义

我们给出逻辑程序（允许在子句体中使用否定-as-失败）语义的纯模型论表述。在我们的语义中，程序的意义是（正如在经典情况下的那样）在程序独立排序中的唯一最小模型。我们使用一个扩充的真值域，其中包含一个包含在 False（最小元素）和 True（最大元素）之间的不可数线性有序的真值集合，中间有一个 Zero 元素。Zero 以下的真值按可数序数排序。Zero 以上的值具有恰好相反的顺序。否定被解释为关于 Zero 后的反射，然后走向 Zero；唯一不受否定影响的真值是 Zero。我们证明每个程序都有一个唯一的最小模型 M_P，并且该模型可以借助一个 T_P 迭代来构建，该迭代穿过可数序数。此外，我们展示 M_P 也可以通过一种模型交叉构造获得，这是对经典逻辑程序模型交叉定理的推广。最后，我们说明通过将无限值模型 M_P 中的 true 和 false 值折叠到（经典的）True 和 False，我们获得的三值模型与 well-founded 模型完全相同。