paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Coalgebraic Geometric Logic: Basic Theory

余代数几何逻辑:基础理论
LMCS vol.Volume 18, Issue 42022匹配度 2/10 · 论文研究余代数几何逻辑的形式语义、推导系统与完备性,属于纯理论逻辑/形式语义工作;与用户核心关注的静态分析、LLM/Agent 交叉、浮点程序分析、贝叶斯程序分析均无直接关联。引用 0 inbox
Nick Bezhanishvili, Jim de Groot, Yde Venema
crossref: 2026-09-10

AI 速览

一句话:用余代数统一框架为命题几何逻辑添加模态,并建立其推导系统、完备性与行为等价理论。

本文借助余代数理论,为命题几何逻辑引入一种统一的模态扩展框架。其模型建立在拓扑空间与连续映射的某个满子范畴上的自函子余代数之上。作者研究此类几何模态逻辑的推导系统、可靠性与完备性,并给出一种方法:将 Set 上的自函子连同谓词提升,提升到拓扑空间范畴,同时保持开谓词提升结构。文章进一步比较所得模型类上的模态等价、行为等价与互模拟,并为相应范畴构造终对象。该工作为几何逻辑与余代数模态逻辑之间建立了基础理论联系。

问题
如何为命题几何逻辑统一地添加模态算子,并在拓扑余代数模型上建立逻辑理论。
方法
采用余代数与谓词提升,把 Set 上的自函子及谓词提升提升到拓扑空间范畴,定义模型与推导系统。
评估
通过证明可靠性与完备性,比较模态等价、行为等价与互模拟,并构造相应范畴的终对象。
原文摘要(Abstract)

Using the theory of coalgebra, we introduce a uniform framework for adding modalities to the language of propositional geometric logic. Models for this logic are based on coalgebras for an endofunctor on some full subcategory of the category of topological spaces and continuous functions. We investigate derivation systems, soundness and completeness for such geometric modal logics, and we specify a method of lifting an endofunctor on Set, accompanied by a collection of predicate liftings, to an endofunctor on the category of topological spaces, again accompanied by a collection of (open) predicate liftings. Furthermore, we compare the notions of modal equivalence, behavioural equivalence and bisimulation on the resulting class of models, and we provide a final object for the corresponding category.

链接与引用

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

BibTeX
@article{paperbot1639,
  title = {Coalgebraic Geometric Logic: Basic Theory},
  author = {Nick Bezhanishvili and Jim de Groot and Yde Venema},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 18, Issue 4},
  year = {2022},
  doi = {10.46298/lmcs-18(4:10)2022}
}