A strictly linear subatomic proof system

DOI10.4230/LIPICS.CSL.2025.39MaRDI QIDQ7261452zbMATH OpenFDO

Authors Victoria Barrett, Alessio Guglielmi, Benjamin Ralph

Publication date 9 June 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.CSL.2025.39

zbMATH Keywords

cut eliminationdecision treesdeep inferenceexplicit substitutionsopen deductionproof theorysubatomic logic

Mathematics Subject Classification ID

Logic in computer science (03B70)

Cites work

• A Local System for Classical Logic
• A Subatomic Proof System for Decision Trees
• A system of interaction and structure
• A System of Interaction and Structure II: The Need for Deep Inference
• Atomic lambda calculus: a typed lambda-calculus with explicit sharing
• From deep inference to proof nets via cut elimination
• Linear unification
• Locality for classical logic
• Normalisation Control in Deep Inference via Atomic Flows
• On the proof complexity of deep inference
• Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
• Removing cycles from proofs
• Subatomic proof systems: splittable systems
• The relative efficiency of propositional proof systems
• Two Restrictions on Contraction

This page was built for publication: A strictly linear subatomic proof system

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7261452)