Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2

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

doi:10.1007/s10817-010-9178-x

Artículo

dc.creator	Martín Mateos, Francisco Jesús	es
dc.creator	Ruiz Reina, José Luis	es
dc.creator	Alonso Jiménez, José Antonio	es
dc.creator	Hidalgo Doblado, María José	es
dc.date.accessioned	2019-05-13T11:32:30Z
dc.date.available	2019-05-13T11:32:30Z
dc.date.issued	2011
dc.identifier.citation	Martín Mateos, F.J., Ruiz Reina, J.L., Alonso Jiménez, J.A. y Hidalgo Doblado, M.J. (2011). Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2. Journal of Automated Reasoning, 47 (3), 229-250.
dc.identifier.issn	0168-7433	es
dc.identifier.uri	https://hdl.handle.net/11441/86293
dc.description.abstract	Higman’s lemma is an important result in infinitary combinatorics, which has been formalized in several theorem provers. In this paper we present a formalization and proof of Higman’s Lemma in the ACL2 theorem prover. Our formalization is based on a proof by Murthy and Russell, where the key termination argument is justified by the multiset relation induced by a well-founded relation. To our knowledge, this is the first mechanization of this proof.	es
dc.description.sponsorship	Ministerio de Ciencia e Innovación MTM2009-13842-C02-02	es
dc.format	application/pdf	es
dc.language.iso	eng	es
dc.publisher	Springer	es
dc.relation.ispartof	Journal of Automated Reasoning, 47 (3), 229-250.
dc.rights	Attribution-NonCommercial-NoDerivatives 4.0 Internacional	*
dc.rights.uri	http://creativecommons.org/licenses/by-nc-nd/4.0/	*
dc.subject	Higman’s lemma	es
dc.subject	Formal proofs	es
dc.subject	ACL2	es
dc.title	Proof Pearl: a Formal Proof of Higman’s Lemma in ACL2	es
dc.type	info:eu-repo/semantics/article	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	MTM2009-13842-C02-02	es
dc.relation.publisherversion	https://link.springer.com/article/10.1007/s10817-010-9178-x	es
dc.identifier.doi	10.1007/s10817-010-9178-x	es
dc.contributor.group	Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento	es
idus.format.extent	22	es
dc.journaltitle	Journal of Automated Reasoning	es
dc.publication.volumen	47	es
dc.publication.issue	3	es
dc.publication.initialPage	229	es
dc.publication.endPage	250	es

Ficheros	Tamaño	Formato	Ver	Descripción
Proof Pearl, a Formal Proof of ...	538.0Kb	[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