paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Modal meet-implication logic

模态交-蕴涵逻辑
LMCS vol.Volume 18, Issue 32022匹配度 1/10 · 论文研究直觉主义交-蕴涵逻辑的模态扩展、半格语义、对偶与完备性,属于纯逻辑与形式语义理论;与用户关注的程序静态分析、LLM/Agent、浮点程序分析及贝叶斯程序分析等方向没有直接关联。引用 1 inbox
Jim de Groot, Dirk Pattinson
crossref: 2026-09-10

AI 速览

一句话:为直觉主义交-蕴涵片段引入保交与单调模态,建立半格语义、对偶、完备性及可表达性结果。

论文研究命题直觉主义逻辑的交-蕴涵片段在加入模态算子后的逻辑性质。作者首先将交-蕴涵片段扩展为带有保交模态的模态逻辑,给出基于半格(semilattice)的语义,并建立与适当描述框架(descriptive frame)的对偶结果。由此证明该逻辑相对该语义的完备性,并识别出一大类模态直觉主义逻辑所共有的模态片段。进一步将该逻辑视为 dialgebraic logic,从而得到“expressivity-somewhere-else”性质。随后在 dialgebraic 框架内考察带单调模态的交-蕴涵片段扩展,证明其完备性并同样建立 expressivity-somewhere-else。

问题
如何在命题直觉主义逻辑的交-蕴涵片段上加入保交模态与单调模态,并刻画其语义、对偶与证明论性质。
方法
采用基于半格的语义与描述框架对偶,并将所得逻辑置于 dialgebraic logic 框架中进行研究。
评估
通过完备性定理和 expressivity-somewhere-else 性质进行评估;这些结果同时覆盖保交模态与单调模态扩展。
原文摘要(Abstract)

We extend the meet-implication fragment of propositional intuitionistic logic with a meet-preserving modality. We give semantics based on semilattices and a duality result with a suitable notion of descriptive frame. As a consequence we obtain completeness and identify a common (modal) fragment of a large class of modal intuitionistic logics. We recognise this logic as a dialgebraic logic, and as a consequence obtain expressivity-somewhere-else. Within the dialgebraic framework, we then investigate the extension of the meet-implication fragment of propositional intuitionistic logic with a monotone modality and prove completeness and expressivity-somewhere-else for it.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1686,
  title = {Modal meet-implication logic},
  author = {Jim de Groot and Dirk Pattinson},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 3},
  year = {2022},
  doi = {10.46298/lmcs-18(3:1)2022}
}