Repositorio de producción científica de la Universidad de Sevilla

A Formal Proof of Dickson’s Lemma in ACL2

 

Advanced Search
 
Opened Access A Formal Proof of Dickson’s Lemma in ACL2
Cites

Show item statistics
Icon
Export to
Author: Martín Mateos, Francisco Jesús
Alonso Jiménez, José Antonio
Hidalgo Doblado, María José
Ruiz Reina, José Luis
Department: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Date: 2003
Published in: LPAR 2003: 10th International Conference on Logic for Programming Artificial Intelligence and Reasoning (2003), p 49-58
ISBN/ISSN: 978-3-540-20101-4
0302-9743
Document type: Presentation
Abstract: Dickson’s Lemma is the main result needed to prove the termination of Buchberger’s algorithm for computing Gr¨obner 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: Martín Mateos, F.J., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Ruiz Reina, J.L. (2003). A Formal Proof of Dickson’s Lemma in ACL2. En LPAR 2003: 10th International Conference on Logic for Programming Artificial Intelligence and Reasoning (49-58), Almaty, Kazakhstan: Springer.
Size: 173.7Kb
Format: PDF

URI: https://hdl.handle.net/11441/86152

DOI: 10.1007/978-3-540-39813-4_3

See editor´s version

This work is under a Creative Commons License: 
Attribution-NonCommercial-NoDerivatives 4.0 Internacional

This item appears in the following Collection(s)