paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Diagrammatic Algebra of First Order Logic

一阶逻辑的图解代数
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 2/10 · 该论文属于纯范畴论/逻辑数学方向，讨论一阶逻辑的弦图演算与完备公理化，既不涉及程序静态分析、浮点或贝叶斯程序分析，也不涉及 LLM/Agent 或工具落地，仅与形式语义、形式化验证在“逻辑基础”层面有非常间接的联系。引用 12 inbox
Filippo Bonchi, Alessandro Di Giorgio, Nathan Haydon, Pawel Sobocinski
形式语义逻辑与自动机
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话：提出新皮尔士关系演算，用弦图给出一阶逻辑表达力的二元关系演算及其完备公理化。

本文研究如何为具有一阶逻辑表达力的关系演算提供图解式公理化。作者引入“新皮尔士关系”（neo-Peircean relations），将经典二元关系演算扩展为弦图演算，并通过组合笛卡尔双范畴与线性双范畴这两类已知范畴结构来刻画其公理。该演算在表达力上等价于一阶逻辑，且给出的公理系统是完备的。论文因此为一阶逻辑提供了一种范畴化、图解化的代数呈现，也展示了双范畴结构在逻辑演算组织中的作用。

问题
如何用弦图/图解代数以范畴结构为具有一阶逻辑表达力的关系演算提供完备公理化？
方法
引入 neo-Peircean relations，将二元关系演算扩展为弦图演算，并组合笛卡尔双范畴与线性双范畴得到公理。
评估
论证该演算与一阶逻辑具有相同表达力，并给出完备公理化。
原文摘要（Abstract）

We introduce the calculus of neo-Peircean relations, a string diagrammatic extension of the calculus of binary relations that has the same expressivity as first order logic and comes with a complete axiomatisation. The axioms are obtained by combining two well known categorical structures: cartesian and linear bicategories.

链接与引用

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

BibTeX 
@inproceedings{abs-2401-07055,
  title = {Diagrammatic Algebra of First Order Logic},
  author = {Filippo Bonchi and Alessandro Di Giorgio and Nathan Haydon and Pawel Sobocinski},
  booktitle = {LICS},
  year = {2024},
  doi = {10.1145/3661814.3662078}
}