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

implicational intuitionistic logicKomori's problemminimal formulasminimal implicational theoremnatural deductionnon-prime contractionuniqueness of normal proofs

Mathematics Subject Classification ID

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

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

(9)

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

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)