Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2
Journal of Automated Reasoning(2010)
摘要
Higman’s lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. In this paper we present a formalization and proof of Higman’s Lemma in the ACL2 theorem prover. Our formalization is based on a proof by Murthy and Russell, where the key termination argument is justified by the multiset relation induced by a well-founded relation. To our knowledge, this is the first mechanization of this proof.
更多查看译文
关键词
Higman's lemma,Formal proofs,ACL2
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要