η-conversions of IPC implemented in atomic F.
Logic Journal of the IGPL（2017）
摘要
It is known that the $\beta$-conversions of the full intuitionistic propositional calculus ( $\mathbf{IPC}$) translate into $\beta\eta$-conversions of the atomic polymorphic calculus ${\mathbf{F}}_{\mathbf{at}}$. Since ${\mathbf{F}}_{\mathbf{at}}$ enjoys the property of strong normalization for $\beta\eta$-conversions, an alternative proof of strong normalization for $\mathbf{IPC}$ considering $\b...
更多查看译文
关键词
η-conversions,predicative polymorphism,intuitionistic propositional calculus,strong normalization,natural deduction
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要