摘要（中文）

本文探讨了破坏模态逻辑（Sabotage Modal Logic，SML）的一些模型和证明论方面的问题。破坏模态逻辑是一种扩展了标准模态语言的新逻辑，增加了边删除模态操作符，表达了“在删除至少一条边后公式成立”的语义。研究的核心贡献包括：

1. 特征定理的证明：将破坏模态逻辑刻画为一阶逻辑中对破坏双模仿（sabotage bisimulation）保持不变的片段。
2. 表格方法的提出：开发了SML的一个可靠且完备的表格方法（tableau method）。
3. 未解问题的讨论：提出了一系列关于破坏模态逻辑的研究方向，包括其与模型更新逻辑的整合、决策性问题的探讨，以及对SML逻辑形式的可能限制。

此外，文章还讨论了破坏模态逻辑与动态认知逻辑和理论计算机科学的联系，特别是在模型检查复杂性及其不可判定性方面的研究进展。

---

Abstract (English)

This paper explores certain model and proof-theoretic aspects of Sabotage Modal Logic (SML). SML extends the standard modal language by introducing an edge-deletion modality that expresses the semantics “after deleting at least one edge, the formula holds.” The main contributions of this study include:

1. Proof of a Characterization Theorem: SML is characterized as the fragment of first-order logic invariant under a specific notion of bisimulation, called sabotage bisimulation.
2. Development of a Tableau Method: A sound and complete tableau method for SML is proposed.
3. Discussion of Open Problems: Several open research questions are raised, including the integration of SML within the current landscape of logics of model update, its decision problems, and potential semantic restrictions.

The paper also discusses the connections of SML with dynamic epistemic logic and theoretical computer science, particularly in terms of model-checking complexity and its undecidability.

Reference:

HAL Id: hal-01194426
https://inria.hal.science/hal-01194426v1