Normalisation Control in Deep Inference via Atomic Flows

Abstract

We introduce `atomic flows': they are graphs obtained from derivations by tracing atom occurrences and forgetting the logical structure. We study simple manipulations of atomic flows that correspond to complex reductions on derivations. This allows us to prove, for propositional logic, a new and very general normalisation theorem, which contains cut elimination as a special case. We operate in deep inference, which is more general than other syntactic paradigms, and where normalisation is more difficult to control. We argue that atomic flows are a significant technical advance for normalisation theory, because 1) the technique they support is largely independent of syntax; 2) indeed, it is largely independent of logical inference rules; 3) they constitute a powerful geometric formalism, which is more intuitive than syntax.

References in corpus (4)

• A System of Interaction and Structure II: The Need for Deep Inference
• Normalisation Control in Deep Inference via Atomic Flows
• From Proof Nets to the Free *-Autonomous Category
• The three dimensions of proofs

Cited by in corpus (7)

• Normalisation Control in Deep Inference via Atomic Flows
• On the Proof Complexity of Deep Inference
• A System of Interaction and Structure IV: The Exponentials and Decomposition
• On the relative proof complexity of deep inference via atomic flows
• Interaction and Depth against Nondeterminism in Proof Search
• Beyond formulas-as-cographs: an extension of Boolean logic to arbitrary graphs
• Enumerating Independent Linear Inferences