Logic beyond formulas: a proof system on graphs

DOI10.1145/3373718.3394763MaRDI QIDQ5145617zbMATH OpenOpenAlexWikidataFDO

Authors Matteo Acclavio, Ross Horne, Lutz Straßburger

Publication date 21 January 2021

Published in Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2012.01102

zbMATH Keywords

analycitycographscut eliminationdeep inferencegraph modulesprime graphsproof theorysplitting

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This means that we lose the tree structure of the formulas corresponding to the cographs, and we can no longer 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 generalisation of the splitting property. Finally, we show that our system is a conservative extension of multiplicative linear logic with mix, and we argue that our graphs form a notion of generalised connective.

Recommendations

• Planar and braided proof-nets for multiplicative linear logic with mix
• scientific article; zbMATH DE number 1231525
• Proof nets of PN as graphs
• Proof nets for unit-free multiplicative-additive linear logic
• A graph-theoretic characterization theorem for multiplicative fragment of non-commutative linear logic

Cited in

(15)

• Linear time proof verification on N-graphs: a graph theoretic approach
• scientific article; zbMATH DE number 5010047 (Why is no real title available?)
• On the Expressive Power of Graph Logic
• On Graph-theoretic Fibring of Logics
• scientific article; zbMATH DE number 1354098 (Why is no real title available?)
• scientific article; zbMATH DE number 2020175 (Why is no real title available?)
• scientific article; zbMATH DE number 6970800 (Why is no real title available?)
• scientific article; zbMATH DE number 7599923 (Why is no real title available?)
• An Analytic Propositional Proof System on Graphs
• scientific article; zbMATH DE number 7809762 (Why is no real title available?)
• Enumerating Independent Linear Inferences
• A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
• A deep inference system for differential linear logic
• Logic programming with multiplicative structures
• Sequent systems on undirected graphs

This page was built for publication: Logic beyond formulas: a proof system on graphs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145617)