Uniqueness of normal proofs in implicational intuitionistic logic

DOI10.1023/A:1008254111992zbMath0931.03067OpenAlexW1562621175MaRDI QIDQ1288178

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)

Related Items

A Datalog Recognizer for Almost Affine λ-CFGs ⋮ Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus ⋮ Studying provability in implicational intuitionistic logic ⋮ On the membership problem for non-linear abstract categorial grammars