Presentation
A Formal Proof of Dickson’s Lemma in ACL2
Author/s | 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 |
Publication Date | 2003 |
Deposit Date | 2019-05-02 |
Published in |
|
ISBN/ISSN | 978-3-540-20101-4 0302-9743 |
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 ... 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. |
Project ID. | TIC2000-1368-C03-02 |
Citation | 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. |
Files | Size | Format | View | Description |
---|---|---|---|---|
A Formal Proof of Dickson's Lemma ... | 173.7Kb | [PDF] | View/ | |