Normalisation Control in Deep Inference via Atomic Flows

DOI10.2168/LMCS-4(1:9)2008zbMath1142.03033arXiv0709.1205MaRDI QIDQ3518275

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 elimination; propositional logic; deep inference; geometric formalism; normalisation theorem

Mathematics Subject Classification ID

03F05: Cut-elimination and normal-form theorems

03B05: Classical propositional logic

Related Items

Unnamed Item, Unnamed Item, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, On Compositionality of Dinatural Transformations, Deep inference and expansion trees for second-order multiplicative linear logic, Combinatorial flows as bicolored atomic flows, Enumerating Independent Linear Inferences, A graphical foundation for interleaving in game semantics, Classical proof forestry, On the decision problem for MELL, Minimal type inference for linked data consumers, True Concurrency of Deep Inference Proofs, 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