An Analytic Propositional Proof System on Graphs

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 generalisation 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 generalised connective.

References in corpus (8)

• A System of Interaction and Structure
• A System of Interaction and Structure II: The Need for Deep Inference
• On the Proof Complexity of Deep Inference
• Subatomic Proof Systems: Splittable Systems
• De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
• Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs
• Relating Reasoning Methodologies in Linear Logic and Process Algebra
• A Deep Inference System for Differential Linear Logic

Cited by in corpus (3)

• A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
• Logic Programming with Multiplicative Structures
• Enumerating Independent Linear Inferences