paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Dual-Context Calculi for Modal Logic

模态逻辑的双上下文演算
LMCS vol.Volume 16, Issue 32020匹配度 1/10 · 该论文属于纯类型论/模态逻辑与范畴语义的基础研究，讨论 K、T、K4、GL、S4 必要性片段的双上下文自然演绎与模态 λ 演算，与用户的静态分析、LLM/Agent、浮点程序分析、贝叶斯程序分析等核心方向均无直接关联；虽同属程序语言理论基础，但既非 LLM 与静态分析交叉，也未经工程落地或工业验证。引用 42 inbox
G. A. Kavvos
类型系统形式语义
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话：为 K、T、K4、GL、S4 的必要性片段建立双上下文自然演绎与模态 λ 演算，并给出范畴语义。

本文为正规模态逻辑 K、T、K4、GL 和 S4 的必要性片段给出一类自然演绎系统及其对应的模态 lambda 演算。这些系统采用双上下文风格，把假设分成模态与直觉主义两个区域，并说明其来源可追溯至相继式演算。作者研究其元理论，构造了合流且强规范化的归约关系，并证明这些演算在可证性意义上与通常的 Hilbert 系统一致。最后，他们考察了一种范畴语义，将模态算子解释为保持乘积的函子。该工作统一了模态逻辑的证明论、类型论与范畴语义视角。

问题
如何为模态逻辑的必要性片段提供具有良好归约性质和类型论解释的自然演绎系统，并刻画其范畴语义。
方法
采用双上下文自然演绎与模态 lambda 演算，建立合流且强规范化的归约，证明其与 Hilbert 系统的可证性等价，并给出将模态解释为保持乘积函子的范畴语义。
评估
通过证明元理论性质（合流、强规范化、可证性等价）以及建立范畴语义模型，来评估系统与既有 Hilbert 演算的一致性。
原文摘要（Abstract）

We present natural deduction systems and associated modal lambda calculi for the necessity fragments of the normal modal logics K, T, K4, GL and S4. These systems are in the dual-context style: they feature two distinct zones of assumptions, one of which can be thought as modal, and the other as intuitionistic. We show that these calculi have their roots in in sequent calculi. We then investigate their metatheory, equip them with a confluent and strongly normalizing notion of reduction, and show that they coincide with the usual Hilbert systems up to provability. Finally, we investigate a categorical semantics which interprets the modality as a product-preserving functor.Comment: Full version of article previously presented at LICS 2017 (see arXiv:1602.04860v4 or doi: 10.1109/LICS.2017.8005089)

链接与引用

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

BibTeX 
@article{Kavvos20,
  title = {Dual-Context Calculi for Modal Logic},
  author = {G. A. Kavvos},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 16, Issue 3},
  year = {2020},
  doi = {10.23638/lmcs-16(3:10)2020}
}