Explicit Composition and Its Application in Proofs of Normalization

DOI10.1007/978-3-319-22686-6_8OpenAlexW2256771682MaRDI QIDQ5864201FDOQ5864201

Authors: Jan von Plato 

Publication date: 3 June 2022

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

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

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

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)

Cited In (4)

• A formalization of Sambins's normalization for GL
• Peano's Counterexample to Harmony
• Normalization Proof for Derivations in PA after P. Cohen
• Title not available (Why is that?)

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)