Classical proof forestry

DOI10.1016/j.apal.2010.04.006zbMath1223.03039MaRDI QIDQ636369

Willem Heijltjes

Publication date: 26 August 2011

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: http://opus.bath.ac.uk/32340/1/Classical_Proof_Forestry.pdf

zbMATH Keywords

proof theory; cut-elimination; classical logic; game semantics; backtracking games

Mathematics Subject Classification ID

03F05: Cut-elimination and normal-form theorems

03F07: Structure of proofs

Related Items

GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION, On the Herbrand content of LK, Expansion trees with cut, Herbrand's theorem as higher order recursion

Cites Work

• Categorical proof theory of classical propositional calculus
• A compact representation of proofs
• Locality for classical logic
• Proofs without syntax
• Order-enriched categorical models of the classical sequent calculus
• Proof Nets for Herbrand’s Theorem
• Normalisation Control in Deep Inference via Atomic Flows
• A new constructive logic: classic logic
• Proof Nets for Classical Logic
• Sequentiality vs. concurrency in games and logic
• Identity of Proofs Based on Normalization and Generality
• A semantics of evidence for classical arithmetic
• Proof Transformations and Structural Invariance
• Proof Identity for Classical Logic: Generalizing to Normality
• Typed Lambda Calculi and Applications