A Formal Proof of Dickson’s Lemma in ACL2

Martín Mateos, Francisco Jesús; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Ruiz Reina, José Luis

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

Ponencia

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

Ficheros	Tamaño	Formato	Ver	Descripción
A Formal Proof of Dickson's Lemma ...	173.7Kb	[PDF]	Ver/Abrir

Este registro aparece en las siguientes colecciones

Artículos (Ciencias de la Computación e Inteligencia Artificial)

Mostrar el registro sencillo del ítem

Excepto si se señala otra cosa, la licencia del ítem se describe como: Attribution-NonCommercial-NoDerivatives 4.0 Internacional