Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof

DOI10.1007/978-3-540-70590-1_28MaRDI QIDQ3522034zbMATH OpenOpenAlexFDO

Authors Christian Urban, Bozhi Zhu

Publication date 28 August 2008

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-70590-1_28

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Grammars and rewriting systems (68Q42)

Recommendations

• scientific article; zbMATH DE number 1722668
• scientific article; zbMATH DE number 1342291
• Cut elimination, substitution and normalisation
• Strong normalisation of cut-elimination in classical logic
• A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs

Cited in

(10)

• Formalized meta-theory of sequent calculi for substructural logics
• A formally verified cut-elimination procedure for linear nested sequents for tense logic
• Book review of: Matthias Baaz and Alexander Leitsch, Methods of cut-elimination
• Formalized meta-theory of sequent calculi for linear logics
• Unwinding a Non-effective Cut Elimination Proof
• scientific article; zbMATH DE number 7178366 (Why is no real title available?)
• General bindings and alpha-equivalence in Nominal Isabelle
• Formalized proof systems for propositional logic
• Facilitating meta-theory reasoning (invited paper)
• Invertibility in Sequent Calculi

Describes a project that uses

Uses Software

• Isabelle/HOL

This page was built for publication: Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3522034)