Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

An Analytic Propositional Proof System On Graphs

Matteo Acclavio 1 Ross Horne 1 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
Abstract : 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 generalization 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 generalized connective.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas

https://hal.inria.fr/hal-03087392
Contributor : Lutz Straßburger <>
Submitted on : Wednesday, December 23, 2020 - 6:32:51 PM
Last modification on : Tuesday, December 29, 2020 - 3:31:36 AM

File

2012.01102.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03087392, version 1

Collections

Citation

Matteo Acclavio, Ross Horne, Lutz Straßburger. An Analytic Propositional Proof System On Graphs. 2020. ⟨hal-03087392⟩

Share

Metrics

Record views

12

Files downloads

89