Normalisation Control in Deep Inference via Atomic Flows

DOI10.2168/LMCS-4(1:9)2008MaRDI QIDQ3518275zbMATH OpenFDO

Authors Alessio Guglielmi, Tom Gundersen

Publication date 7 August 2008

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

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

zbMATH Keywords

cut eliminationdeep inferencegeometric formalismnormalisation theorempropositional logic

Mathematics Subject Classification ID

Classical propositional logic (03B05) Cut-elimination and normal-form theorems (03F05)

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.

Recommendations

• Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
• Complexity of Deep Inference via Atomic Flows
• On the relative proof complexity of deep inference via atomic flows
• A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
• Logical Approaches to Computational Barriers

Cited in

(24)

• On the decision problem for MELL
• Minimal type inference for linked data consumers
• True concurrency of deep inference proofs
• Complexity of Deep Inference via Atomic Flows
• On the Power of Substitution in the Calculus of Structures
• On linear rewriting systems for Boolean logic and some applications to proof theory
• On the proof complexity of cut-free bounded deep inference
• Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
• Transformations via Geometric Perspective Techniques Augmented with Cycles Normalization
• A graphical foundation for interleaving in game semantics
• On Compositionality of Dinatural Transformations
• The sub-additives: a proof theory for probabilistic choice extending linear logic
• scientific article; zbMATH DE number 7204450 (Why is no real title available?)
• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
• Deep inference and expansion trees for second-order multiplicative linear logic
• Quasipolynomial Normalisation in Deep Inference via Atomic Flows and Threshold Formulae
• Logical Approaches to Computational Barriers
• Normalization flow
• Combinatorial flows as bicolored atomic flows
• Enumerating Independent Linear Inferences
• Classical proof forestry
• Focusing Gentzen's LK proof system
• Deep inference in proof search: the need for shallow inference
• A strictly linear subatomic proof system

This page was built for publication: Normalisation Control in Deep Inference via Atomic Flows

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