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

DOI10.1007/978-3-540-70590-1_28zbMath1146.68041OpenAlexW1961313574MaRDI QIDQ3522034

Bozhi Zhu, Christian Urban

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)

Related Items (5)

A formally verified cut-elimination procedure for linear nested sequents for tense logic ⋮ Formalized meta-theory of sequent calculi for linear logics ⋮ Unnamed Item ⋮ Formalized meta-theory of sequent calculi for substructural logics ⋮ General Bindings and Alpha-Equivalence in Nominal Isabelle

Uses Software

• Isabelle/HOL

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