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

linear logiclambda calculuscut-eliminationnormalisationcontraction rulenotation systemsterm-rewriting

Mathematics Subject Classification ID

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)

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

(20)

• Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• SN and CR for free-style LK^tq: linear decorations and simulation of normalization
• scientific article; zbMATH DE number 7447752 (Why is no real title available?)
• On the form of witness terms
• scientific article; zbMATH DE number 1722668 (Why is no real title available?)
• 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
• Some general results about proof normalization
• Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof
• Strong normalisation in the \(\pi\)-calculus
• The computational content of arithmetical proofs
• Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
• 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

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)