paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Logic Beyond Formulas

超越公式的逻辑
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 1/10 · 该论文属于纯证明论/线性逻辑的形式化工作,研究图上推理、cut 可容许与 MLL+mix 保守扩展,与用户核心方向(静态分析、LLM/Agent 与 PL 交叉、浮点/贝叶斯程序分析)没有直接关联。虽然涉及形式化验证的理论基础,但不面向程序分析、ML 系统、LLM/Agent 或工业落地。引用 8 inbox
Matteo Acclavio, Ross Horne, Lutz Straßburger
crossref: 2026-09-12

AI 速览

一句话:提出直接在图上推理的证明系统,用模块分解与深推理证明 cut 可容许,并保守扩展 MLL+mix。

论文提出一种直接作用于图而非公式的证明系统。作者从公式与 cograph(不以 P4 为诱导子图的无向图)的经典对应出发,取消该限制,转向任意无向图。由于公式的树结构随之丢失,依赖树结构的标准证明论方法不再适用。为此,论文采用图的模块分解以及深推理技术,使推理规则不依赖公式主连接词。系统被证明具有 cut 可容许性,并满足分裂性质的推广。最后,作者证明该系统和带 mix 的乘法线性逻辑(MLL+mix)相比是保守扩张:若一个 cograph 在该系统中可证,则它在 MLL+mix 中也可证。

问题
如何为不依赖公式树结构的图证明系统建立证明论,特别是将公式与 cograph 的对应推广到任意无向图。
方法
利用图的模块分解和 deep inference 技术,构造直接操作于任意无向图的证明系统,并证明 cut 可容许性与广义 splitting 性质。
评估
通过证明该系统是 MLL+mix 的保守扩张来评估:若 cograph 在系统中可证,则其在 MLL+mix 中也可证。
原文摘要(Abstract)

In this paper we present a proof system that operates on graphs instead of formulas. We begin our quest with the well-known correspondence between formulas and cographs, which are undirected graphs that do not have P4 (the four-vertex path) as vertex-induced subgraph; and then we drop that condition and look at arbitrary (undirected) graphs. The consequence is that we lose the tree structure of the formulas corresponding to the cographs. Therefore we cannot use standard proof theoretical methods that depend on that tree structure. In order to overcome this difficulty, we use a modular decomposition of graphs and some techniques from deep inference where inference rules do not rely on the main connective of a formula. For our proof system we show the admissibility of cut and a generalization of the splitting property. Finally, we show that our system is a conservative extension of multiplicative linear logic (MLL) with mix, meaning that if a graph is a cograph and provable in our system, then it is also provable in MLL+mix.

链接与引用

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

BibTeX
@inproceedings{paperbot5495,
  title = {Logic Beyond Formulas},
  author = {Matteo Acclavio and Ross Horne and Lutz Straßburger},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394763}
}