Strong normalisation of cut-elimination in classical logic
From MaRDI portal
Publication:2708321
zbMATH Open0982.03032MaRDI QIDQ2708321FDOQ2708321
Publication date: 14 March 2002
Published in: Fundamenta Informaticae (Search for Journal in Brave)
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 (17)
- 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
- Cut Elimination, Substitution and Normalisation
- Categorical proof theory of classical propositional calculus
- 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
- Revisiting Zucker’s Work on the Correspondence Between Cut-Elimination and Normalisation
- A minimal classical sequent calculus free of structural rules
- Expansion trees with cut
- A strong normalization result for classical logic
- Proof nets for classical logic
Recommendations
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)
