Uniqueness of normal proofs in implicational intuitionistic logic

DOI10.1023/A:1008254111992MaRDI QIDQ1288178zbMATH OpenOpenAlexFDO

Authors Takahito Aoto

Publication date 20 June 1999

Published in Journal of Logic, Language and Information (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1008254111992

zbMATH Keywords

natural deductionimplicational intuitionistic logicKomori's problemminimal formulasminimal implicational theoremnon-prime contractionuniqueness of normal proofs

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Recommendations

• Uniqueness of normal proofs of minimal formulas
• scientific article; zbMATH DE number 700345
• Studying provability in implicational intuitionistic logic: the formula tree approach

Cited in

(6)

• A Datalog recognizer for almost affine \(\lambda \)-CFGs
• Game semantics and uniqueness of type inhabitance in the simply-typed \(\lambda \)-calculus
• Studying provability in implicational intuitionistic logic: the formula tree approach
• Uniqueness of normal proofs of minimal formulas
• On the membership problem for non-linear abstract categorial grammars
• scientific article; zbMATH DE number 517044 (Why is no real title available?)

This page was built for publication: Uniqueness of normal proofs in implicational intuitionistic logic

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