## Abstract

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 language | English |
---|---|

Title of host publication | Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 |

Pages | 38-52 |

Number of pages | 15 |

ISBN (Electronic) | 9781450371049 |

DOIs | |

Publication status | Published - 8 Jul 2020 |

Event | 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 - Saarbrucken, Germany Duration: 8 Jul 2020 → 11 Jul 2020 https://lics.siglog.org/lics20/#:~:text=The%20LICS%20Symposium%20is%20an,co%2Dlocation%20with%20ICALP%202020. |

### Publication series

Name | ACM International Conference Proceeding Series |
---|

### Conference

Conference | 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 |
---|---|

Abbreviated title | LICS 2020 |

Country/Territory | Germany |

City | Saarbrucken |

Period | 8/07/20 → 11/07/20 |

Internet address |

## Keywords

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