Towards Non-Monotonic Entailment in Propositional Defeasible Standpoint Logic

技术摘要：迈向命题可撤销立场逻辑中的非单调蕴涵

问题陈述
近期在可撤销推理方面的进展已成功将偏好语义和 KLM 式蕴涵应用于模态逻辑，特别是命题可撤销立场逻辑（PDSL）。PDSL 允许使用诸如 $❘∼∼❘_e \alpha$（意为“在立场 $e$ 最典型的理解中，$\alpha$ 成立”）之类的模态算子，在单一框架内表示冲突的观点和典型信念。然而，该领域现有的工作主要集中在可满足性检查和 Tarskian（单调）蕴涵（$\models_P$）上。

作者指出当前单调方法存在一个关键的推理缺陷。在 $\models_P$ 下，知识库往往无法支持直觉上的非单调推理。例如，如果一个立场 $P$ 通常相信 $\alpha$，且 $\alpha$ 可撤销地蕴涵 $\beta$，那么单调框架无法得出 $P$ 通常相信 $\beta$ 的结论。同样，子立场（例如工程学）无法从超立场（例如物理学）继承典型信念，只要存在任何潜在的冲突，即使目前不存在具体的冲突也是如此。这限制了 PDSL 在预期进行继承和典型性推理的原型推理中的效用。

方法论
为了解决这些局限性，本文提出将传统的命题 KLM 推理中的非单调理性蕴涵关系提升（lifting）到 PDSL 的一个片段中。该方法论通过四个主要阶段进行：

1. 通过情境条件句扩展表达能力：
   作者引入了“情境立场条件句”，形式为 $\alpha \rightsquigarrow_e \beta$，读作“在立场 $e$ 内，对 $\alpha$ 的信念通常意味着对 $\beta$ 的信念”。这种构造允许将可撤销蕴涵特异地定位在某个立场的语境中，而非全局性的。作者证明了这种新语法足以重新刻画整个 PDSL 语言，有效地用这些情境条件句和通用立场模态（$\square_*$）取代了标准的撤销模态和蕴涵。

2. 向命题 KLM 转换：
   论文定义了一个特定的 PDSL 片段，记作 $Cond(\tilde{\mathcal{L}}_S)$，它由正向可撤销条件句（$\alpha \rightsquigarrow_e \beta$）和立场细化（$e \lesssim d$）组成。定义了一个转换函数 $T$，将该片段中的公式映射到传统的命题 KLM 条件知识库。

   • 立场表达式被转换为命题原子或其布尔组合。
   • 条件句 $\alpha \rightsquigarrow_e \beta$ 被转换为 $(\alpha \land t(e)) \mid\sim \beta$。
   • 立场细化 $e \lesssim d$ 被转换为 $t(e) \mid\sim t(d)$。
     至关重要的是，作者证明了这种转换是忠实的：一个 PDSL 知识库是可满足的，当且仅当其命题转换也是可满足的，且模型满足关系在转换下得以保持（$M \models \varphi \iff T(M) \models T(\varphi)$）。

3. 提升蕴涵关系：
   利用转换函数 $T$，作者将命题情况下的理性可撤销蕴涵关系提升到 PDSL 情况。对于给定的排名策略 $r$（它为知识库分配一个排名函数），PDSL 中的蕴涵关系 $| \approx_r$ 定义为：$\mathcal{K} | \approx_r \varphi$ 当且仅当命题排名模型 $r(T(\mathcal{K}))$ 的前像满足 $\varphi$。
   这种方法允许使用现有的命题算法（如 DefeasibleEntail）来执行 PDSL 中的蕴涵检查。

4. 具体实例化：
   该框架应用于两个著名的理性蕴涵系统：

   • 理性闭包（Rational Closure）： 通过最小排名函数定义。论文表明，PDSL 中的理性闭包避免了单调蕴涵的推理缺陷，允许在不存在直接冲突的情况下继承典型信念。
   • 列举式闭包（Lexicographic Closure）： 引入用于解决“淹没问题”（即一个属性中的异常会阻碍无关典型信念的继承）。作者证明，PDSL 中的列举式闭包能够成功区分无关信念，允许子立场继承那些未涉及特定异常的信念。

主要结果

• 表达能力： 情境条件句的引入使得 PDSL 能够使用类似于命题条件句的结构来表达其完整语法，从而促进向 KLM 逻辑的转换。
• 推理强度： 所提出的非单调蕴涵（$| \approx_r$）严格强于之前的单调蕴涵（$\models_P$）。它成功支持了子立场的典型信念继承以及从典型信念中导出后果，而 $\models_P$ 则无法做到这一点。
• 复杂度保持： 所提 PDSL 片段的蕴涵检查复杂度与命题情况相同。
  • 检查理性闭包是 $P^{NP}_{||}$-完全的。
  • 检查列举式闭包是 $P^{NP}$-完全的。
  • 这是通过线性转换 $T$ 以及可以直接使用底层命题算法实现的。
• 处理菱形模态： 论文引入了一个“否定作为失败”算子（not）来处理非单调框架内的菱形模态（$\Diamond_e \alpha$）。这允许关于可能性的“勇敢推理”（brave reasoning）：如果一种可能性未被知识库排除，则认为其成立。

意义与主张
论文声称提供了一种将非单调推理集成到立场逻辑中的系统化方法，解决了以往单调方法“推理能力薄弱”的问题。通过建立 PDSL 片段与命题 KLM 逻辑之间的忠实转换，作者使得直接应用成熟的理性蕴涵系统（理性闭包和列举式闭包）于多视角推理成为可能。

其意义在于：

1. 解决推理缺陷： 使 PDSL 能够进行原型推理，即子立场可以继承典型信念，且可撤销蕴涵可以在特定的视角内传播。
2. 解决淹没问题： 证明了可以通过应用列举式闭包于 PDSL，以防止无关的异常阻碍典型信念的继承。
3. 计算效率： 证明了这些高级非单调推理可以使用现有的命题算法进行计算，而不会增加计算复杂度类。

作者总结道，他们的工作弥合了立场逻辑的表达能力与 KLM 式可撤销推理的鲁棒推理能力之间的鸿沟，提供了一个处理冲突和典型视角的实用框架。