paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A Real-Valued Modal Logic

一种实值模态逻辑
LMCS vol.Volume 14, Issue 12018匹配度 2/10 · 该论文是纯模态逻辑/证明论工作（实值 Kripke 语义、标签 tableau、coNEXPTIME 上界、切消除），与用户核心方向（LLM/Agent 与静态分析的交叉、浮点程序分析、贝叶斯程序分析）没有直接关联；仅在“实数格/证明论工具”这一非常间接的层面可能与程序分析形式化沾边，且不含工程实现或 benchmark 层面的内容。引用 6 inbox
Denisa Diaconescu, George Metcalfe, Laura Schnüriger
逻辑与自动机定理证明与证明工程
crossref: 2026-09-10

AI 速览

一句话：提出基于实数格与群运算的实值模态逻辑，给出带标签 tableau、coNEXPTIME 上界，并建立乘性片段的切消除与公理化。

本文引入一种实值模态逻辑，将标准模态逻辑 K 的 Kripke 框架语义与实数上的格运算和群运算相结合，在世界局部解释模态连接词。作者为该系统设计带标签的 tableau 证明系统，并据此证明判定公式有效性的复杂度上界为 coNEXPTIME。随后聚焦模态-乘性片段，利用该 tableau 系统证明一个允许切消除的序贯演算的完备性，同时给出一个扩展 Abelian 逻辑乘性片段的公理系统，并证明其完备性。该工作将多值语义、模态逻辑与证明论方法结合，为实值模态推理提供了可判定性与证明系统基础。

问题
如何在保留 Kripke 框架语义的同时，用实数上的格与群运算在世界局部解释模态连接词，并刻画所得多值模态逻辑的有效性、复杂度与证明系统。
方法
引入实值模态逻辑并设计带标签 tableau 系统；聚焦模态-乘性片段，构造带切消除的序贯演算和扩展 Abelian 逻辑乘性片段的公理系统。
评估
证明有效性检查具有 coNEXPTIME 上界，并建立序贯演算与公理系统相对给定语义的完备性以及切消除。
原文摘要（Abstract）

A many-valued modal logic is introduced that combines the usual Kripke frame semantics of the modal logic K with connectives interpreted locally at worlds by lattice and group operations over the real numbers. A labelled tableau system is provided and a coNEXPTIME upper bound obtained for checking validity in the logic. Focussing on the modal-multiplicative fragment, the labelled tableau system is then used to establish completeness for a sequent calculus that admits cut-elimination and an axiom system that extends the multiplicative fragment of Abelian logic.

链接与引用

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

BibTeX 
@article{paperbot432,
  title = {A Real-Valued Modal Logic},
  author = {Denisa Diaconescu and George Metcalfe and Laura Schnüriger},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 14, Issue 1},
  year = {2018},
  doi = {10.23638/lmcs-14(1:10)2018}
}