{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:11Z","timestamp":1753894391251,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,10,21]],"date-time":"2022-10-21T00:00:00Z","timestamp":1666310400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>In this paper we present a proof system that operates on graphs instead of\nformulas. Starting from the well-known relationship between formulas and\ncographs, we drop the cograph-conditions and look at arbitrary undirected)\ngraphs. This means that we lose the tree structure of the formulas\ncorresponding to the cographs, and we can no longer use standard proof\ntheoretical methods that depend on that tree structure. In order to overcome\nthis difficulty, we use a modular decomposition of graphs and some techniques\nfrom deep inference where inference rules do not rely on the main connective of\na formula. For our proof system we show the admissibility of cut and a\ngeneralisation of the splitting property. Finally, we show that our system is a\nconservative extension of multiplicative linear logic with mix, and we argue\nthat our graphs form a notion of generalised connective.<\/jats:p>","DOI":"10.46298\/lmcs-18(4:1)2022","type":"journal-article","created":{"date-parts":[[2022,10,24]],"date-time":"2022-10-24T12:14:55Z","timestamp":1666613695000},"source":"Crossref","is-referenced-by-count":2,"title":["An Analytic Propositional Proof System on Graphs"],"prefix":"10.46298","volume":"Volume 18, Issue 4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0425-2825","authenticated-orcid":false,"given":"Matteo","family":"Acclavio","sequence":"first","affiliation":[]},{"given":"Ross","family":"Horne","sequence":"additional","affiliation":[]},{"given":"Lutz","family":"Stra\u00dfburger","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2022,10,21]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/10186\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/10186\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:18:54Z","timestamp":1687292334000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/6957"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,21]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(4:1)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2012.01102v4","asserted-by":"subject"},{"id-type":"arxiv","id":"2012.01102v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2012.01102v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2012.01102","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2012.01102","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2022,10,21]]},"article-number":"6957"}}