Logic beyond formulas: a proof system on graphs

Matteo Acclavio, Ross Horne, Lutz Straßburger

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

7 Citations (Scopus)
19 Downloads (Pure)


In this paper we present a proof system that operates on graphs instead of formulas. We begin our quest with the well-known correspondence between formulas and cographs, which are undirected graphs that do not have P4 (the four-vertex path) as vertex-induced subgraph; and then we drop that condition and look at arbitrary (undirected) graphs. The consequence is that we lose the tree structure of the formulas corresponding to the cographs. Therefore we cannot 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 generalization of the splitting property. Finally, we show that our system is a conservative extension of multiplicative linear logic (MLL) with mix, meaning that if a graph is a cograph and provable in our system, then it is also provable in MLL+mix.

Original languageEnglish
Title of host publicationProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
Number of pages15
ISBN (Electronic)9781450371049
Publication statusPublished - 8 Jul 2020
Event35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 - Saarbrucken, Germany
Duration: 8 Jul 202011 Jul 2020

Publication series

NameACM International Conference Proceeding Series


Conference35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
Abbreviated titleLICS 2020
Internet address


  • analycity
  • cographs
  • cut elimination
  • deep inference
  • graph modules
  • prime graphs
  • Proof theory
  • splitting


Dive into the research topics of 'Logic beyond formulas: a proof system on graphs'. Together they form a unique fingerprint.

Cite this