paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A van Benthem Theorem for Fuzzy Modal Logic

模糊模态逻辑的 van Benthem 定理
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 1/10 · 该论文属于纯数理逻辑（模糊模态逻辑与 van Benthem 定理的量化版本），研究的是双模拟不变性与模态片段的表达能力刻画，与用户关注的静态分析、Agentic 程序、浮点程序分析、贝叶斯程序分析及其与 LLM 的交叉均无直接关联。虽标签含“形式语义”，但并未涉及程序验证工具、benchmark 或工程实现。引用 1 inbox
Paul Wild, Lutz Schröder, Dirk Pattinson, Barbara König
逻辑与自动机形式语义
crossref: 2026-09-12

AI 速览

一句话：证明了模糊一阶逻辑中相对于双模拟距离非扩张的公式恰可由模糊模态公式逼近。

van Benthem 定理经典地刻画了命题模态逻辑是一阶逻辑中双模拟不变的片段。本文将其推广到模糊（定量）情形：在一阶模糊谓词逻辑及其模态片段上，引入自然的双模拟距离概念。主要结果是，模糊一阶公式若相对于该双模拟距离是非扩张的，则恰好是那些能被模糊模态公式逼近的公式。由此给出了模糊模态逻辑的模型论刻画，把经典的双模拟不变性结果提升到定量语义框架，为模糊/定量模态逻辑的表达力提供了统一解释。

问题
经典 van Benthem 定理以双模拟不变性刻画模态逻辑；本文要问在模糊/定量语义下，相应的模态片段能否由双模拟距离的非扩张性刻画。
方法
在一阶模糊谓词逻辑及其模态片段中定义自然的双模拟距离，并证明相对于该距离非扩张的模糊一阶公式与可由模糊模态公式逼近的公式类相等。
评估
评估方式是模型论证明，关键结果是建立模糊一阶逻辑非扩张片段与模糊模态逻辑可逼近性之间的精确对应。
原文摘要（Abstract）

We present a fuzzy (or quantitative) version of the van Benthem theorem, which characterizes propositional modal logic as the bisimulation-invariant fragment of first-order logic. Specifically, we consider a first-order fuzzy predicate logic along with its modal fragment, and show that the fuzzy first-order formulas that are non-expansive w.r.t. the natural notion of bisimulation distance are exactly those that can be approximated by fuzzy modal formulas.

链接与引用

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

BibTeX 
@inproceedings{paperbot4344,
  title = {A van Benthem Theorem for Fuzzy Modal Logic},
  author = {Paul Wild and Lutz Schröder and Dirk Pattinson and Barbara König},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209180}
}