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...
Main Authors: | , , |
---|---|
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 |