Proof Pearl: Wellfounded Induction on the Ordinals Up to ε 0

2007.

被引用0|引用|浏览0|来源

摘要

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.

代码

数据

您的评分 :
0

 

标签
评论