非单调推理系统的插值定理

克雷格插值定理（Craig 1957）是命题逻辑和一阶逻辑中一个重要的定理。它指出，如果公式 $\beta$ 逻辑上遵循公式 $\alpha$，那么存在一个公式 $\gamma$，仅包含同时出现在 $\alpha$ 和 $\beta$ 中的符号，使得 $\beta$ 逻辑上遵循 $\gamma$，且 $\gamma$ 逻辑上遵循 $\alpha$。此类定理对于理解这些逻辑以及加速基于这些逻辑的理论推理具有重要意义。本文针对三个非单调系统提出了类似精神的插值定理：限定逻辑、缺省逻辑和具有稳定模型语义（又称回答集语义）的逻辑程序。这些结果使我们更好地理解这些逻辑，尤其是与其非单调特性形成对比。它们表明，尽管这些逻辑缺乏经典单调性，但某种“单调性”原则仍然成立。此外，它们有时允许我们使用分解推理的方法来处理这些系统，可能提高其适用性和可操作性。最后，它们使我们能够构建使用这些逻辑的结构化表示。