paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Some constructive variants of S4 with the finite model property

具有有限模型性质的一些构造性 S4 变体
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 1/10 · 该论文研究构造性模态逻辑变体（CS4、GS4、S4I）的有限模型性质，属于纯逻辑与自动机理论，未涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向。虽然形式逻辑可为形式化验证提供基础，但与该研究画像的直接关联很弱。引用 8 inbox
Philippe Balbiani, Martin Dieguez, David Fernandez-Duque
逻辑与自动机
crossref: 2026-09-12

AI 速览

一句话：证明了 CS4 具有有限模型性质，并引入 GS4 与 S4I，证明三者均具有有限模型性质。

CS4 和 IS4 是模态逻辑 S4 的直觉主义变体，它们是否具有有限模型性质曾是一个长期未决问题。本文围绕 IS4 引入两个密切相关的逻辑：GS4 是在 IS4 上添加 Gödel-Dummett 公理得到；S4I 则是将模态关系与直觉主义关系的角色互换。作者随后证明 CS4、GS4 和 S4I 均具有有限模型性质。这一结果解决了 CS4 的有限模型性质问题，并为相关构造性模态逻辑的模型论性质提供了新认识。

问题
CS4 与 IS4 作为 S4 的直觉主义变体，其有限模型性质长期未决；本文关注 CS4 及与 IS4 密切相关的构造性变体。
方法
作者引入 GS4（在 IS4 上添加 Gödel-Dummett 公理）和 S4I（交换模态关系与直觉主义关系的角色），并证明这些逻辑具有有限模型性质。
评估
评估方式是逻辑证明：证明 CS4、GS4 与 S4I 均满足有限模型性质。
原文摘要（Abstract）

The logics CS4 and IS4 are intuitionistic variants of the modal logic S4. Whether the finite model property holds for each of these logics has been a long-standing open problem. In this paper we introduce two logics closely related to IS4: GS4, obtained by adding the Gödel-Dummett axiom to IS4, and S4I, obtained by reversing the roles of the modal and intuitionistic relations. We then prove that CS4, GS4, and S4I all enjoy the finite model property.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot6190,
  title = {Some constructive variants of S4 with the finite model property},
  author = {Philippe Balbiani and Martin Dieguez and David Fernandez-Duque},
  booktitle = {LICS},
  year = {2021},
  doi = {10.1109/lics52264.2021.9470643}
}