Strong normalisation of cut-elimination in classical logic
zbMATH Open0982.03032MaRDI QIDQ2708321FDOQ2708321
Authors: C. Urban, Gavin M. Bierman 
Publication date: 14 March 2002
Published in: Fundamenta Informaticae (Search for Journal in Brave)
Recommendations
linear logiclambda calculuscut-eliminationnormalisationcontraction rulenotation systemsterm-rewriting
Cut-elimination and normal-form theorems (03F05) Grammars and rewriting systems (68Q42) Combinatory logic and lambda calculus (03B40) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52)
Cited In (20)
- Title not available (Why is that?)
- Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
- On the form of witness terms
- Title not available (Why is that?)
- Proof theory in the abstract
- A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types
- Categorical proof theory of classical propositional calculus
- Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
- Some general results about proof normalization
- Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
- The computational content of arithmetical proofs
- Strong normalisation in the \(\pi\)-calculus
- A minimal classical sequent calculus free of structural rules
- Strong Normalisation of Cut-Elimination That Simulates β-Reduction
- Expansion trees with cut
- Cut elimination, substitution and normalisation
- A strong normalization result for classical logic
- Proof nets for classical logic
- Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
- SN and CR for free-style LKtq: linear decorations and simulation of normalization
This page was built for publication: Strong normalisation of cut-elimination in classical logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2708321)
