图上的分析命题证明系统
摘要：基于图形而非公式的一种证明系统 摘要：在本文中，我们提出了一种在图形而非公式上操作的证明系统。从已知的公式和半图之间的关系出发，我们放弃了半图条件，而是研究了任意的无向图。这意味着我们失去了与半图相对应的公式的树结构，因此无法使用依赖于该树结构的标准证明方法。为了克服这个困难，我们使用了图形的模块化分解和一些来自深度推理的技术，其中推理规则不依赖于公式的主要连接符。对于我们的证明系统，我们展示了割和分裂性质的可接受性。最后，我们展示了我们的系统是可乘性线性逻辑的多样化扩展，并论证了我们的图形形成了广义连接符的概念。
作者：Matteo Acclavio, Ross Horne and Lutz Stra{ss}burger
论文ID：2012.01102
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22