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.
This work has been supported by project TIC2000-1368-C03-02 (Ministry of Science and Technology, Spain) and FEDER funds.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Becker, T., Weispfenning, V.: Gröbner Bases: A Computational Approach to Commutative Algebra. Springer, Heidelberg (1998)
Berger, U., Schwichtenberg, H., Seisenberger, M.: The Warshall Algorithm and Dickson’s Lemma: Two Examples of Realistic Program Extraction. Journal of Automated Reasoning 26, 205–221 (2001)
Coquand, T., Persson, H.: Gröbner Bases in Type Theory. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol. 1657, pp. 33–46. Springer, Heidelberg (1999)
Dershowitz, N., Manna, Z.: Proving Termination with Multiset Orderings. Communications of the ACM 22(8), 465–476 (1979)
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)
Kaufmann, M., Moore, J.S.: ACL2 Version 2.7 (2001), Homepage: http://www.cs.utexas.edu/users/moore/acl2/
Lee, G., Rudnicki, P.: Dickson’s Lemma. Journal of Formalized Mathematics 14 (2002)
Medina–Bulo, I., Alonso, J.A., Palomo, F.: Polynomial algorithms in ACL2 (an approach to Buchberger algorithm). In: I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial, IDEIA 2002 (2002) (in spanish), Available at http://www.cs.us.es/ideia
Perdry, H.: Strong noetherianity: a new constructive proof of Hilbert’s basis theorem, Available at http://perdry.free.fr/StrongNoetherianity.ps
Persson, H.: An Integrated Development of Buchberger’s Algorithm in Coq. Rapport de recherche de l’INRIA, n (4271) (2001)
Pottier, L.: Dixon’s lemma (1996), Available at ftp://ftp-sop.inria.fr/lemme/Loic.Pottier/MON/
Ruiz–Reina, J.L., Alonso, J.A., Hidalgo, M.J., Martín, F.J.: Multiset Relations: a Tool for Proving Termination. In: Second ACL2 Workshop, Technical Report TR-00-29, Computer Science Departament, University of Texas (2000), Available at http://www.cs.utexas.edu/users/moore/acl2/workshop-2000/
Simpson, S.G.: Ordinal numbers and the Hilbert basis theorem. Journal of Symbolic Logic 53(3), 961–974 (1988)
Sustyk, M.: Proof of Dickson’s Lemma Using the ACL2 Theorem Prover via an Explicit Ordinal Mapping. In: Fourth ACL2 Workshop (2003), Available at http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/
Théry, L.: A Machine-Checked Implementation of Buchberger’s Algorithm. Journal of Automated Reasoning 26(2), 107–137 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
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: Vardi, M.Y., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2003. Lecture Notes in Computer Science(), vol 2850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39813-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-540-39813-4_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20101-4
Online ISBN: 978-3-540-39813-4
eBook Packages: Springer Book Archive