Skip to Main content Skip to Navigation
Conference papers

Logic beyond formulas: a proof system on graphs

Matteo Acclavio 1, 2, 3, 4 Ross Horne 5 Lutz Straßburger 2
2 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
3 METHODES-SAMOVAR - Méthodes et modèles pour les réseaux
SAMOVAR - Services répartis, Architectures, MOdélisation, Validation, Administration des Réseaux
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 P 4 (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.
Document type :
Conference papers
Complete list of metadata

Cited literature [45 references]  Display  Hide  Download
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Friday, May 1, 2020 - 6:58:01 AM
Last modification on : Friday, April 30, 2021 - 10:00:28 AM


Files produced by the author(s)



Matteo Acclavio, Ross Horne, Lutz Straßburger. Logic beyond formulas: a proof system on graphs. LICS 2020 - 35th ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken, Germany. pp.38-52, ⟨10.1145/3373718.3394763⟩. ⟨hal-02560105⟩



Les métriques sont temporairement indisponibles