Abstract
Dickson's Lemma is the main result needed to prove the termination of Buchberger's algorithm for computing Gröbner 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.
Cite
CITATION STYLE
Martín-Mateos, F. J., Alonso, J. A., Hidalgo, M. J., & Ruiz-Reina, J. L. (2003). A formal proof of Dickson’s Lemma in ACL2. In Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) (Vol. 2850, pp. 49–58). Springer Verlag. https://doi.org/10.1007/978-3-540-39813-4_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
