Explicit Composition and Its Application in Proofs of Normalization

DOI10.1007/978-3-319-22686-6_8MaRDI QIDQ5864201OpenAlexFDO

Authors Jan von Plato

Publication date 3 June 2022

Published in Advances in Proof-Theoretic Semantics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-319-22686-6_8

zbMATH Keywords

natural deductionstrong normalizationbar inductionexplicit composition

Mathematics Subject Classification ID

Philosophical and critical aspects of logic and foundations (03A05) Proof theory in general (including proof-theoretic semantics) (03F03) Structure of proofs (03F07) Intuitionistic mathematics (03F55)

Recommendations

• scientific article; zbMATH DE number 874672
• scientific article; zbMATH DE number 1107623
• scientific article; zbMATH DE number 3950526
• Some general results about proof normalization
• Normalisation by completeness with Heyting algebras
• scientific article; zbMATH DE number 4091495
• A new normal form for the compositions of morphisms and inverse morphisms
• Normalization, approximation, and semantics for combinator systems
• scientific article; zbMATH DE number 2019855
• Normal proofs, cut free derivations and structural rules

Cited in

(4)

• Peano's Counterexample to Harmony
• Normalization Proof for Derivations in PA after P. Cohen
• A formalization of Sambins's normalization for GL
• scientific article; zbMATH DE number 598799 (Why is no real title available?)

This page was built for publication: Explicit Composition and Its Application in Proofs of Normalization

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