Proof pearl: wellfounded induction on the ordinals up to Ɛ0
TPHOLs'07 Proceedings of the 20th international conference on Theorem proving in higher order logics（2007）
摘要
We discuss a proof of the wellfounded induction theorem for the ordinals up to Ɛ0. The proof is performed on the embedding of ACL2 in HOL-4, thus providing logical justification for that embedding and supporting the claim that the ACL2 logic has a model.
更多查看译文
关键词
ACL2 logic,logical justification,proof pearl,wellfounded induction theorem
AI 理解论文
溯源树
样例
生成溯源树，研究论文发展脉络
Chat Paper
正在生成论文摘要