A Formal Proof of Dickson's Lemma in ACL2

摘要

Dickson's Lemma is the main result needed to prove the termination of Buchberger's algorithm for computing Groebner basis of polynomial ideals. In this case study, we present a formal proof of Dickson's Lemma using the ACL2 system. Due to the limited expressiveness of the ACL2 logic, the classical non-constructive proof of this result cannot be done in ACL2. Instead, we formalize a proof where the termination argument is justified by the multiset extension of a well-founded relation.