An Analytic Propositional Proof System on Graphs

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 correspond...

Full description

Bibliographic Details
Main Authors: Matteo Acclavio, Ross Horne, Lutz Straßburger
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2022-10-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/6957/pdf
_version_ 1797268508125429760
author Matteo Acclavio
Ross Horne
Lutz Straßburger
author_facet Matteo Acclavio
Ross Horne
Lutz Straßburger
author_sort Matteo Acclavio
collection DOAJ
description 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.
first_indexed 2024-04-25T01:33:35Z
format Article
id doaj.art-9a5cd77a529e4910a92897d33825b2e8
institution Directory Open Access Journal
issn 1860-5974
language English
last_indexed 2024-04-25T01:33:35Z
publishDate 2022-10-01
publisher Logical Methods in Computer Science e.V.
record_format Article
series Logical Methods in Computer Science
spelling doaj.art-9a5cd77a529e4910a92897d33825b2e82024-03-08T10:40:29ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742022-10-01Volume 18, Issue 410.46298/lmcs-18(4:1)20226957An Analytic Propositional Proof System on GraphsMatteo Acclaviohttps://orcid.org/0000-0002-0425-2825Ross HorneLutz StraßburgerIn 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.https://lmcs.episciences.org/6957/pdfcomputer science - logic in computer science
spellingShingle Matteo Acclavio
Ross Horne
Lutz Straßburger
An Analytic Propositional Proof System on Graphs
Logical Methods in Computer Science
computer science - logic in computer science
title An Analytic Propositional Proof System on Graphs
title_full An Analytic Propositional Proof System on Graphs
title_fullStr An Analytic Propositional Proof System on Graphs
title_full_unstemmed An Analytic Propositional Proof System on Graphs
title_short An Analytic Propositional Proof System on Graphs
title_sort analytic propositional proof system on graphs
topic computer science - logic in computer science
url https://lmcs.episciences.org/6957/pdf
work_keys_str_mv AT matteoacclavio ananalyticpropositionalproofsystemongraphs
AT rosshorne ananalyticpropositionalproofsystemongraphs
AT lutzstraßburger ananalyticpropositionalproofsystemongraphs
AT matteoacclavio analyticpropositionalproofsystemongraphs
AT rosshorne analyticpropositionalproofsystemongraphs
AT lutzstraßburger analyticpropositionalproofsystemongraphs