dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Alonso Jiménez, José Antonio | es |
dc.creator | Hidalgo Doblado, María José | es |
dc.creator | Ruiz Reina, José Luis | es |
dc.date.accessioned | 2019-05-02T09:40:34Z | |
dc.date.available | 2019-05-02T09:40:34Z | |
dc.date.issued | 2003 | |
dc.identifier.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. | |
dc.identifier.isbn | 978-3-540-20101-4 | es |
dc.identifier.issn | 0302-9743 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86152 | |
dc.description.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. | es |
dc.description.sponsorship | Ministerio de Ciencia y Tecnología TIC2000-1368-C03-02 | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | LPAR 2003: 10th International Conference on Logic for Programming Artificial Intelligence and Reasoning (2003), p 49-58 | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | A Formal Proof of Dickson’s Lemma in ACL2 | es |
dc.type | info:eu-repo/semantics/conferenceObject | es |
dcterms.identifier | https://ror.org/03yxnpp24 | |
dc.type.version | info:eu-repo/semantics/submittedVersion | es |
dc.rights.accessRights | info:eu-repo/semantics/openAccess | es |
dc.contributor.affiliation | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial | es |
dc.relation.projectID | TIC2000-1368-C03-02 | es |
dc.relation.publisherversion | https://link.springer.com/chapter/10.1007/978-3-540-39813-4_3 | es |
dc.identifier.doi | 10.1007/978-3-540-39813-4_3 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 10 | es |
dc.publication.initialPage | 49 | es |
dc.publication.endPage | 58 | es |
dc.eventtitle | LPAR 2003: 10th International Conference on Logic for Programming Artificial Intelligence and Reasoning | es |
dc.eventinstitution | Almaty, Kazakhstan | es |
dc.relation.publicationplace | Berlin | es |