Matteo Acclavio ; Ross Horne ; Lutz Straßburger - An Analytic Propositional Proof System on Graphs

lmcs:6957 - Logical Methods in Computer Science, October 21, 2022, Volume 18, Issue 4 - https://doi.org/10.46298/lmcs-18(4:1)2022
An Analytic Propositional Proof System on GraphsArticle

Authors: Matteo Acclavio ORCID; Ross Horne ; Lutz Straßburger

    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.


    Volume: Volume 18, Issue 4
    Published on: October 21, 2022
    Accepted on: September 9, 2022
    Submitted on: December 4, 2020
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Incentive - LA 1 - 2013; Funder: Fundação para a Ciência e a Tecnologia, I.P.; Code: Incentivo/SAU/LA0001/2013

    1 Document citing this article

    Consultation statistics

    This page has been seen 1805 times.
    This article's PDF has been downloaded 443 times.