An Analytic Propositional Proof System on Graphs

DOI10.46298/lmcs-18(4:1)2022OpenAlexW3110522991WikidataQ114985621 ScholiaQ114985621MaRDI QIDQ5060181

Lutz Straßburger, Ross Horne, Matteo Acclavio

Publication date: 9 January 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2012.01102v6

zbMATH Keywords

cut eliminationsplittinganalyticityproof theoryprime graphsdeep inference

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items

An Analytic Propositional Proof System on Graphs, Enumerating Independent Linear Inferences, A System of Interaction and Structure III: The Complexity of BV and Pomset Logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A survey of the algorithmic aspects of modular decomposition
• Linear logic
• Modeling concurrency with partial orders
• Natural deduction and coherence for weakly distributive categories
• Petri nets, event structures and domains. I
• The structure of multiplicatives
• Handsome proof-nets: Perfect matchings and cographs
• Series-parallel languages and the bounded-width property
• On the length of medial-switch-mix derivations
• Untersuchungen über das logische Schliessen. I
• Untersuchungen über das logische Schliessen. II
• Linear concurrent constraint programming: Operational and phase semantics
• MELL in the calculus of structures
• A formal framework for specifying sequent calculus proof systems
• Non decomposable connectives of linear logic
• On concurrent behaviors and focusing in linear logic
• Topology of series-parallel networks
• On subexponentials, focusing and modalities in concurrent systems
• Proofs without syntax
• The modular decomposition of countable graphs. Definition and construction in monadic second-order logic
• Uniform proofs as a foundation for logic programming
• A deep inference system for the modal logic S5
• On the proof complexity of deep inference
• On linear rewriting systems for Boolean logic and some applications to proof theory
• A Local System for Classical Logic
• A system of interaction and structure V: the exponentials and splitting
• A CUT-FREE SIMPLE SEQUENT CALCULUS FOR MODAL LOGIC S5
• Logic Programming with Focusing Proofs in Linear Logic
• The relative efficiency of propositional proof systems
• The mix rule
• Subnets of proof-nets in multiplicative linear logic with MIX
• Subatomic Proof Systems
• The Consistency and Complexity of Multiplicative Additive System Virtual
• De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
• Pomset Logic
• An Analytic Propositional Proof System on Graphs
• Logic Beyond Formulas
• Constructing weak simulations from linear implications for processes with private names
• A system of interaction and structure
• No complete linear term rewriting system for propositional logic
• A System of Interaction and Structure II: The Need for Deep Inference
• Algorithm Theory - SWAT 2004
• A Proof Calculus Which Reduces Syntactic Bureaucracy
• Transitiv orientierbare Graphen
• Relating reasoning methodologies in linear logic and process algebra
• Generalized connectives for multiplicative linear logic
• BV and Pomset Logic Are Not the Same
• New Minimal Linear Inferences in Boolean Logic Independent of Switch and Medial