Strong normalisation of cut-elimination in classical logic

MaRDI QIDQ2708321zbMATH OpenFDO

Authors C. Urban, Gavin M. Bierman

Publication date 14 March 2002

Published in Fundamenta Informaticae (Search for Journal in Brave)

zbMATH Keywords

contraction rulecut-eliminationlambda calculuslinear logicnormalisationnotation systemsterm-rewriting

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Grammars and rewriting systems (68Q42)

Recommendations

• scientific article; zbMATH DE number 1342291
• scientific article; zbMATH DE number 1722668
• A short proof of the strong normalization of classical natural deduction with disjunction
• A strong normalization result for classical logic
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction

Cited in

(22)

• The computational content of arithmetical proofs
• A strong normalization result for classical logic
• Some general results about proof normalization
• Proof nets for classical logic
• scientific article; zbMATH DE number 1722668 (Why is no real title available?)
• A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types
• scientific article; zbMATH DE number 7447752 (Why is no real title available?)
• Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
• scientific article; zbMATH DE number 1302675 (Why is no real title available?)
• scientific article; zbMATH DE number 1342291 (Why is no real title available?)
• SN and CR for free-style LK^tq: linear decorations and simulation of normalization
• Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
• Cut elimination, substitution and normalisation
• Expansion trees with cut
• Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• Proof theory in the abstract
• Strong normalisation in the \(\pi\)-calculus
• A minimal classical sequent calculus free of structural rules
• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• Categorical proof theory of classical propositional calculus
• On the form of witness terms

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)